The cow is blue. The mouse chases the cow. The squirrel needs the tiger. The tiger is round. If someone needs the mouse and the mouse chases the tiger then the mouse needs the squirrel. If someone needs the mouse then the mouse likes the tiger. If someone likes the tiger and they need the squirrel then the tiger likes the squirrel. If someone is blue then they need the tiger. If someone likes the mouse then they chase the tiger. If someone is blue then they like the mouse. If someone is blue and kind then they chase the mouse. If someone chases the tiger then they need the cow.
The cow is blue.
("cow" "is" "blue" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone needs the mouse and the mouse chases the tiger then the mouse needs the squirrel.
((("someone" "needs" "mouse" "+") ("mouse" "chases" "tiger" "+")) -> ("mouse" "needs" "squirrel" "+"))
If someone needs the mouse then the mouse likes the tiger.
((("someone" "needs" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone likes the tiger and they need the squirrel then the tiger likes the squirrel.
((("someone" "likes" "tiger" "+") ("someone" "needs" "squirrel" "+")) -> ("tiger" "likes" "squirrel" "+"))
If someone is blue then they need the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "tiger" "+"))
If someone likes the mouse then they chase the tiger.
((("someone" "likes" "mouse" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is blue then they like the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is blue and kind then they chase the mouse.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the tiger then they need the cow.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "cow" "+"))
The tiger is round.
True
1
proof
[(triple4)]
("tiger" "is" "round" "+")
triple4
The squirrel does not need the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "needs" "tiger" "-")
triple3
The cow likes the mouse.
True
2
proof
[(((triple1) -> rule6))]
("cow" "likes" "mouse" "+")
((triple1) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "likes" "mouse" "-")
((triple1) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow chases the tiger.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "chases" "tiger" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "chases" "tiger" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not need the cow.
Unknown
inv-rconc
[@3: The tiger needs the cow.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule6 <- FAIL)]]
("tiger" "needs" "cow" "-")
The tiger needs the mouse.
Unknown
random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "+")
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cow is blue.[(triple1)] The mouse chases the cow.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger is round.[(triple4)] @1: The cow likes the mouse.[(((triple1) -> rule6))] The cow needs the tiger.[(((triple1) -> rule4))] @2: The cow chases the tiger.[(((((triple1) -> rule6)) -> rule5))] @3: The cow needs the cow.[(((((((triple1) -> rule6)) -> rule5)) -> rule8))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple1) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple1) -> (rule4 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3