The cow eats the tiger. The tiger is round. If someone is nice then they eat the cow. If someone is round then they like the tiger. If someone is big and red then they need the tiger. If someone eats the cow and they eat the tiger then they need the tiger. If someone eats the tiger then they like the cow. If someone likes the cow then they eat the cow.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone is nice then they eat the cow.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "cow" "+"))
If someone is round then they like the tiger.
((("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is big and red then they need the tiger.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the cow and they eat the tiger then they need the tiger.
((("someone" "eats" "cow" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the tiger then they like the cow.
((("someone" "eats" "tiger" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they eat the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "eats" "cow" "+"))
The cow eats the tiger.
True
1
proof
[(triple1)]
("cow" "eats" "tiger" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "-")
triple2
The tiger likes the tiger.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "likes" "tiger" "+")
((triple2) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "likes" "tiger" "-")
((triple2) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("cow" "eats" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("cow" "eats" "cow" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow needs the tiger.
True
5
proof
[(((((((triple1) -> rule5)) -> rule6) triple1) -> rule4))]
("cow" "needs" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow does not need the tiger.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule6) triple1) -> rule4))]
("cow" "needs" "tiger" "-")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The tiger does not like the cow.
Unknown
inv-rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "cow" "-")
The cow likes the tiger.
Unknown
rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "tiger" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger eats the cow.
Unknown
rconc
[@2: The tiger eats the cow.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("tiger" "eats" "cow" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
@0: The cow eats the tiger.[(triple1)] The tiger is round.[(triple2)] @1: The cow likes the cow.[(((triple1) -> rule5))] The tiger likes the tiger.[(((triple2) -> rule2))] @2: The cow eats the cow.[(((((triple1) -> rule5)) -> rule6))] @3: The cow needs the tiger.[(((((((triple1) -> rule5)) -> rule6) triple1) -> rule4))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple2
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple2) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3