The cow is nice. The cow needs the tiger. The cow sees the tiger. The tiger is big. The tiger needs the cow. The tiger sees the cow. The tiger visits the cow. If someone needs the tiger and they are nice then they need the cow. If someone needs the cow and the cow sees the tiger then they visit the cow.
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone needs the tiger and they are nice then they need the cow.
((("someone" "needs" "tiger" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow and the cow sees the tiger then they visit the cow.
((("someone" "needs" "cow" "+") ("cow" "sees" "tiger" "+")) -> ("someone" "visits" "cow" "+"))
The tiger needs the cow.
True
1
proof
[(triple5)]
("tiger" "needs" "cow" "+")
triple5
The cow does not see the tiger.
False
1
inv-proof
[(triple3)]
("cow" "sees" "tiger" "-")
triple3
The cow needs the cow.
True
3
proof
[(((triple2 triple1) -> rule1))]
("cow" "needs" "cow" "+")
((triple2 triple1) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("cow" "needs" "cow" "-")
((triple2 triple1) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
True
5
proof
[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
("cow" "visits" "cow" "+")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not visit the cow.
False
5
inv-proof
[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
("cow" "visits" "cow" "-")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The cow is nice.[(triple1)] The cow needs the tiger.[(triple2)] The cow sees the tiger.[(triple3)] The tiger is big.[(triple4)] The tiger needs the cow.[(triple5)] The tiger sees the cow.[(triple6)] The tiger visits the cow.[(triple7 OR ((triple5 triple3) -> rule2))] @1: The cow needs the cow.[(((triple2 triple1) -> rule1))] @2: The cow visits the cow.[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple3
The tiger is big.
("tiger" "is" "big" "+")
triple4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple5
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
((triple5 triple3) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2 triple1) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2