The cow eats the tiger. The cow needs the tiger. The tiger is blue. If something eats the cow then it does not need the cow. If something is rough and it eats the tiger then the tiger is blue. If something needs the cow and it is not cold then it is round. All blue things are rough. If something is nice and round then it does not chase the tiger. If something needs the cow then the cow does not eat the tiger.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something eats the cow then it does not need the cow.
((("something" "eats" "cow" "+")) -> ("something" "needs" "cow" "-"))
If something is rough and it eats the tiger then the tiger is blue.
((("something" "is" "rough" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something needs the cow and it is not cold then it is round.
((("something" "needs" "cow" "+") ("something" "is" "cold" "~")) -> ("something" "is" "round" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is nice and round then it does not chase the tiger.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "chases" "tiger" "-"))
If something needs the cow then the cow does not eat the tiger.
((("something" "needs" "cow" "+")) -> ("cow" "eats" "tiger" "-"))
The tiger is blue.
True
1
proof
[(triple3)]
("tiger" "is" "blue" "+")
triple3
The cow does not need the tiger.
False
1
inv-proof
[(triple2)]
("cow" "needs" "tiger" "-")
triple2
The tiger is rough.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "is" "rough" "-")
((triple3) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "round" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The tiger chases the cow.
Unknown
random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "+")
@0: The cow eats the tiger.[(triple1)] The cow needs the tiger.[(triple2)] The tiger is blue.[(triple3)] @1: The tiger is rough.[(((triple3) -> rule4))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1