The cat does not chase the dog. The cat is big. The cat likes the cow. The cat does not like the tiger. The cat sees the tiger. The cow likes the cat. The cow likes the dog. The dog chases the cat. The dog chases the cow. The dog does not chase the tiger. The dog is not round. The dog sees the cow. The tiger chases the dog. The tiger does not like the cat. The tiger sees the cat. If the dog chases the tiger and the tiger is not round then the tiger is blue. If something likes the dog and it sees the cow then it chases the dog. If something sees the cow then the cow sees the cat. If the cat is young then the cat sees the cow. If the cow sees the cat then the cow is not round. If something is round and it does not chase the dog then it chases the cat.
The cat does not chase the dog.
("cat" "chases" "dog" "-")
The cat is big.
("cat" "is" "big" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
The dog is not round.
("dog" "is" "round" "-")
The dog sees the cow.
("dog" "sees" "cow" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the dog chases the tiger and the tiger is not round then the tiger is blue.
((("dog" "chases" "tiger" "+") ("tiger" "is" "round" "~")) -> ("tiger" "is" "blue" "+"))
If something likes the dog and it sees the cow then it chases the dog.
((("something" "likes" "dog" "+") ("something" "sees" "cow" "+")) -> ("something" "chases" "dog" "+"))
If something sees the cow then the cow sees the cat.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "cat" "+"))
If the cat is young then the cat sees the cow.
((("cat" "is" "young" "+")) -> ("cat" "sees" "cow" "+"))
If the cow sees the cat then the cow is not round.
((("cow" "sees" "cat" "+")) -> ("cow" "is" "round" "-"))
If something is round and it does not chase the dog then it chases the cat.
((("something" "is" "round" "+") ("something" "chases" "dog" "~")) -> ("something" "chases" "cat" "+"))
The cow likes the dog.
True
1
proof
[(triple7)]
("cow" "likes" "dog" "+")
triple7
The dog does not chase the cat.
False
1
inv-proof
[(triple8)]
("dog" "chases" "cat" "-")
triple8
The cow sees the cat.
True
2
proof
[(((triple12) -> rule3))]
("cow" "sees" "cat" "+")
((triple12) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow does not see the cat.
False
2
inv-proof
[(((triple12) -> rule3))]
("cow" "sees" "cat" "-")
((triple12) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is not round.
True
3
proof
[(((((triple12) -> rule3)) -> rule5))]
("cow" "is" "round" "-")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is round.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule5))]
("cow" "is" "round" "+")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The tiger does not chase the cat.
Unknown
inv-rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "cat" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "blue" "+")
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "dog" "-")
The tiger chases the cow.
Unknown
random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "+")
The tiger does not like the cow.
Unknown
inv-random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cat does not chase the dog.[(triple1)] The cat does not like the tiger.[(triple4)] The cat is big.[(triple2)] The cat likes the cow.[(triple3)] The cat sees the tiger.[(triple5)] The cow likes the cat.[(triple6)] The cow likes the dog.[(triple7)] The dog chases the cat.[(triple8)] The dog chases the cow.[(triple9)] The dog does not chase the tiger.[(triple10)] The dog is not round.[(triple11)] The dog sees the cow.[(triple12)] The tiger chases the dog.[(triple13)] The tiger does not like the cat.[(triple14)] The tiger sees the cat.[(triple15)] @1: The cow sees the cat.[(((triple12) -> rule3))] @2: The cow is not round.[(((((triple12) -> rule3)) -> rule5))]
The cat does not chase the dog.
("cat" "chases" "dog" "-")
triple1
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
triple4
The cat is big.
("cat" "is" "big" "+")
triple2
The cat likes the cow.
("cat" "likes" "cow" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow likes the dog.
("cow" "likes" "dog" "+")
triple7
The dog chases the cat.
("dog" "chases" "cat" "+")
triple8
The dog chases the cow.
("dog" "chases" "cow" "+")
triple9
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
triple10
The dog is not round.
("dog" "is" "round" "-")
triple11
The dog sees the cow.
("dog" "sees" "cow" "+")
triple12
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple13
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The cow sees the cat.
("cow" "sees" "cat" "+")
((triple12) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is not round.
("cow" "is" "round" "-")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2