The cat does not eat the cow. The cat is not red. The cow is kind. The cow is round. The cow needs the cat. The tiger chases the cat. The tiger chases the cow. The tiger does not eat the cat. The tiger eats the cow. The tiger is red. The tiger is round. The tiger needs the cow. If someone needs the tiger then they do not eat the tiger. If the tiger needs the cow then the cow chases the tiger. If someone chases the tiger then they chase the cow.
The cat does not eat the cow.
("cat" "eats" "cow" "-")
The cat is not red.
("cat" "is" "red" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone needs the tiger then they do not eat the tiger.
((("someone" "needs" "tiger" "+")) -> ("someone" "eats" "tiger" "-"))
If the tiger needs the cow then the cow chases the tiger.
((("tiger" "needs" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If someone chases the tiger then they chase the cow.
((("someone" "chases" "tiger" "+")) -> ("someone" "chases" "cow" "+"))
The cow needs the cat.
True
1
proof
[(triple5)]
("cow" "needs" "cat" "+")
triple5
The cow is not round.
False
1
inv-proof
[(triple4)]
("cow" "is" "round" "-")
triple4
The cow chases the tiger.
True
2
proof
[(((triple12) -> rule2))]
("cow" "chases" "tiger" "+")
((triple12) -> (rule2 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow does not chase the tiger.
False
2
inv-proof
[(((triple12) -> rule2))]
("cow" "chases" "tiger" "-")
((triple12) -> (rule2 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow chases the cow.
True
3
proof
[(((((triple12) -> rule2)) -> rule3))]
("cow" "chases" "cow" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow does not chase the cow.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule3))]
("cow" "chases" "cow" "-")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cat does not chase the cow.
Unknown
inv-rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cow" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cat does not chase the tiger.
Unknown
inv-random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The cat does not eat the cow.[(triple1)] The cat is not red.[(triple2)] The cow is kind.[(triple3)] The cow is round.[(triple4)] The cow needs the cat.[(triple5)] The tiger chases the cat.[(triple6)] The tiger chases the cow.[(triple7)] The tiger does not eat the cat.[(triple8)] The tiger eats the cow.[(triple9)] The tiger is red.[(triple10)] The tiger is round.[(triple11)] The tiger needs the cow.[(triple12)] @1: The cow chases the tiger.[(((triple12) -> rule2))] @2: The cow chases the cow.[(((((triple12) -> rule2)) -> rule3))]
The cat does not eat the cow.
("cat" "eats" "cow" "-")
triple1
The cat is not red.
("cat" "is" "red" "-")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow needs the cat.
("cow" "needs" "cat" "+")
triple5
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple7
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple8
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple12) -> (rule2 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2