The cow is big. The cow is blue. The mouse chases the cow. The mouse is blue. The mouse likes the cow. The tiger is nice. The tiger needs the mouse. If something chases the tiger then the tiger chases the mouse. If the cow likes the tiger then the cow needs the tiger. If something needs the tiger then it likes the mouse. If something is blue and it likes the cow then the cow likes the mouse. If something chases the cow then the cow is red. If something is blue and it needs the tiger then the tiger chases the cow. If something needs the cow then it is young. If something is red then it chases the tiger.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something chases the tiger then the tiger chases the mouse.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If the cow likes the tiger then the cow needs the tiger.
((("cow" "likes" "tiger" "+")) -> ("cow" "needs" "tiger" "+"))
If something needs the tiger then it likes the mouse.
((("something" "needs" "tiger" "+")) -> ("something" "likes" "mouse" "+"))
If something is blue and it likes the cow then the cow likes the mouse.
((("something" "is" "blue" "+") ("something" "likes" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If something chases the cow then the cow is red.
((("something" "chases" "cow" "+")) -> ("cow" "is" "red" "+"))
If something is blue and it needs the tiger then the tiger chases the cow.
((("something" "is" "blue" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If something needs the cow then it is young.
((("something" "needs" "cow" "+")) -> ("something" "is" "young" "+"))
If something is red then it chases the tiger.
((("something" "is" "red" "+")) -> ("something" "chases" "tiger" "+"))
The mouse is blue.
True
1
proof
[(triple4)]
("mouse" "is" "blue" "+")
triple4
The mouse does not chase the cow.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "cow" "-")
triple3
The cow is red.
True
2
proof
[(((triple3) -> rule5))]
("cow" "is" "red" "+")
((triple3) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow does not like the mouse.
False
3
inv-proof
[(((triple4 triple5) -> rule4))]
("cow" "likes" "mouse" "-")
((triple4 triple5) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The mouse chases the tiger.
Unknown
rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is big.[(triple1)] The cow is blue.[(triple2)] The mouse chases the cow.[(triple3)] The mouse is blue.[(triple4)] The mouse likes the cow.[(triple5)] The tiger is nice.[(triple6)] The tiger needs the mouse.[(triple7)] @1: The cow is red.[(((triple3) -> rule5))] The cow likes the mouse.[(((triple4 triple5) -> rule4))] @2: The cow chases the tiger.[(((((triple3) -> rule5)) -> rule8))] @3: The tiger chases the mouse.[(((((((triple3) -> rule5)) -> rule8)) -> rule1))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple5
The tiger is nice.
("tiger" "is" "nice" "+")
triple6
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple7
The cow is red.
("cow" "is" "red" "+")
((triple3) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple4 triple5) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((((triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3