The cow eats the tiger. The rabbit visits the tiger. The tiger is young. If something is kind then it is rough. If something likes the cow and it is not kind then it is green. If the rabbit is young and the rabbit is blue then the rabbit visits the cow. If something eats the tiger then it eats the cow. If something is young and it visits the rabbit then it visits the cow. If something is young then it eats the tiger. If something visits the rabbit and it is not green then the rabbit likes the tiger. If something likes the tiger and it does not eat the rabbit then the tiger is not blue.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something likes the cow and it is not kind then it is green.
((("something" "likes" "cow" "+") ("something" "is" "kind" "~")) -> ("something" "is" "green" "+"))
If the rabbit is young and the rabbit is blue then the rabbit visits the cow.
((("rabbit" "is" "young" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "visits" "cow" "+"))
If something eats the tiger then it eats the cow.
((("something" "eats" "tiger" "+")) -> ("something" "eats" "cow" "+"))
If something is young and it visits the rabbit then it visits the cow.
((("something" "is" "young" "+") ("something" "visits" "rabbit" "+")) -> ("something" "visits" "cow" "+"))
If something is young then it eats the tiger.
((("something" "is" "young" "+")) -> ("something" "eats" "tiger" "+"))
If something visits the rabbit and it is not green then the rabbit likes the tiger.
((("something" "visits" "rabbit" "+") ("something" "is" "green" "~")) -> ("rabbit" "likes" "tiger" "+"))
If something likes the tiger and it does not eat the rabbit then the tiger is not blue.
((("something" "likes" "tiger" "+") ("something" "eats" "rabbit" "~")) -> ("tiger" "is" "blue" "-"))
The tiger is young.
True
1
proof
[(triple3)]
("tiger" "is" "young" "+")
triple3
The tiger is not young.
False
1
inv-proof
[(triple3)]
("tiger" "is" "young" "-")
triple3
The cow eats the cow.
True
2
proof
[(((triple1) -> rule4))]
("cow" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple3) -> rule6))]
("tiger" "eats" "tiger" "-")
((triple3) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the cow.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("tiger" "eats" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger does not eat the cow.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("tiger" "eats" "cow" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "cow" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "green" "+")
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The cow eats the tiger.[(triple1)] The rabbit visits the tiger.[(triple2)] The tiger is young.[(triple3)] @1: The cow eats the cow.[(((triple1) -> rule4))] The tiger eats the tiger.[(((triple3) -> rule6))] @2: The tiger eats the cow.[(((((triple3) -> rule6)) -> rule4))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple3) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2