The cow likes the mouse. The cow likes the rabbit. The cow visits the mouse. The cow visits the rabbit. The mouse chases the rabbit. The mouse is red. The mouse likes the cow. The mouse visits the rabbit. The rabbit visits the cow. The rabbit visits the mouse. If someone visits the rabbit then they are big. If the cow is nice and the cow is kind then the cow likes the mouse. If the cow visits the mouse then the cow is blue. If someone is red and they like the mouse then they visit the cow. If someone is big then they chase the cow. If someone chases the cow and the cow likes the mouse then they visit the mouse.
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone visits the rabbit then they are big.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "big" "+"))
If the cow is nice and the cow is kind then the cow likes the mouse.
((("cow" "is" "nice" "+") ("cow" "is" "kind" "+")) -> ("cow" "likes" "mouse" "+"))
If the cow visits the mouse then the cow is blue.
((("cow" "visits" "mouse" "+")) -> ("cow" "is" "blue" "+"))
If someone is red and they like the mouse then they visit the cow.
((("someone" "is" "red" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "visits" "cow" "+"))
If someone is big then they chase the cow.
((("someone" "is" "big" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow and the cow likes the mouse then they visit the mouse.
((("someone" "chases" "cow" "+") ("cow" "likes" "mouse" "+")) -> ("someone" "visits" "mouse" "+"))
The mouse chases the rabbit.
True
1
proof
[(triple5)]
("mouse" "chases" "rabbit" "+")
triple5
The rabbit does not visit the cow.
False
1
inv-proof
[(triple9)]
("rabbit" "visits" "cow" "-")
triple9
The mouse is big.
True
2
proof
[(((triple8) -> rule1))]
("mouse" "is" "big" "+")
((triple8) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "is" "big" "-")
((triple4) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the cow.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("cow" "chases" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The mouse does not chase the cow.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule5))]
("mouse" "chases" "cow" "-")
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse visits the mouse.
True
5
proof
[(((((((triple8) -> rule1)) -> rule5) triple1) -> rule6))]
("mouse" "visits" "mouse" "+")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse does not visit the mouse.
False
5
inv-proof
[(((((((triple8) -> rule1)) -> rule5) triple1) -> rule6))]
("mouse" "visits" "mouse" "-")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse does not visit the cow.
Unknown
inv-rconc
[@1: The mouse visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "cow" "-")
The rabbit chases the cow.
Unknown
rconc
[@2: The rabbit chases the cow.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("rabbit" "chases" "cow" "+")
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "big" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cow" "+")
The rabbit does not like the cow.
Unknown
inv-random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "-")
The cow chases the mouse.
Unknown
random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cow likes the mouse.[(triple1)] The cow likes the rabbit.[(triple2)] The cow visits the mouse.[(triple3 OR ((((((triple4) -> rule1)) -> rule5) triple1) -> rule6))] The cow visits the rabbit.[(triple4)] The mouse chases the rabbit.[(triple5)] The mouse is red.[(triple6)] The mouse likes the cow.[(triple7)] The mouse visits the rabbit.[(triple8)] The rabbit visits the cow.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The cow is big.[(((triple4) -> rule1))] The cow is blue.[(((triple3) -> rule3) OR ((((((((triple4) -> rule1)) -> rule5) triple1) -> rule6)) -> rule3))] The mouse is big.[(((triple8) -> rule1))] @2: The cow chases the cow.[(((((triple4) -> rule1)) -> rule5))] The mouse chases the cow.[(((((triple8) -> rule1)) -> rule5))] @3: The mouse visits the mouse.[(((((((triple8) -> rule1)) -> rule5) triple1) -> rule6))]
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The cow is big.
("cow" "is" "big" "+")
((triple4) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
((triple8) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3