The cow visits the mouse. The mouse chases the cow. The mouse is cold. The mouse is nice. The mouse is not rough. The mouse does not need the cow. The mouse visits the cow. If something visits the cow and it visits the mouse then the cow chases the mouse. If something needs the mouse then the mouse visits the cow. If something is cold then it visits the cow. If something visits the cow and it chases the cow then it is nice. If something visits the cow then the cow is cold. If something chases the cow and the cow needs the mouse then the cow is round.
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something visits the cow and it visits the mouse then the cow chases the mouse.
((("something" "visits" "cow" "+") ("something" "visits" "mouse" "+")) -> ("cow" "chases" "mouse" "+"))
If something needs the mouse then the mouse visits the cow.
((("something" "needs" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If something is cold then it visits the cow.
((("something" "is" "cold" "+")) -> ("something" "visits" "cow" "+"))
If something visits the cow and it chases the cow then it is nice.
((("something" "visits" "cow" "+") ("something" "chases" "cow" "+")) -> ("something" "is" "nice" "+"))
If something visits the cow then the cow is cold.
((("something" "visits" "cow" "+")) -> ("cow" "is" "cold" "+"))
If something chases the cow and the cow needs the mouse then the cow is round.
((("something" "chases" "cow" "+") ("cow" "needs" "mouse" "+")) -> ("cow" "is" "round" "+"))
The mouse chases the cow.
True
1
proof
[(triple2)]
("mouse" "chases" "cow" "+")
triple2
The mouse does not visit the cow.
False
1
inv-proof
[(triple7 OR ((triple3) -> rule3))]
("mouse" "visits" "cow" "-")
triple7
((triple3) -> (rule3 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow is cold.
True
2
proof
[(((triple7) -> rule5) OR ((((triple3) -> rule3)) -> rule5))]
("cow" "is" "cold" "+")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow is not cold.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((triple3) -> rule3)) -> rule5))]
("cow" "is" "cold" "-")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the cow.
True
3
proof
[(((((triple7) -> rule5)) -> rule3) OR ((((((triple3) -> rule3)) -> rule5)) -> rule3))]
("cow" "visits" "cow" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The cow does not visit the cow.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule3) OR ((((((triple3) -> rule3)) -> rule5)) -> rule3))]
("cow" "visits" "cow" "-")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The cow chases the mouse.
True
5
proof
[(((((((triple7) -> rule5)) -> rule3) triple1) -> rule1) OR ((((((((triple3) -> rule3)) -> rule5)) -> rule3) triple1) -> rule1))]
("cow" "chases" "mouse" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int4
The cow does not chase the mouse.
False
5
inv-proof
[(((((((triple7) -> rule5)) -> rule3) triple1) -> rule1) OR ((((((((triple3) -> rule3)) -> rule5)) -> rule3) triple1) -> rule1))]
("cow" "chases" "mouse" "-")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int4
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "nice" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "round" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cow visits the mouse.[(triple1)] The mouse chases the cow.[(triple2)] The mouse does not need the cow.[(triple6)] The mouse is cold.[(triple3)] The mouse is nice.[(triple4 OR ((triple7 triple2) -> rule4) OR ((((triple3) -> rule3) triple2) -> rule4))] The mouse is not rough.[(triple5)] The mouse visits the cow.[(triple7 OR ((triple3) -> rule3))] @1: The cow is cold.[(((triple7) -> rule5) OR ((((triple3) -> rule3)) -> rule5))] @2: The cow visits the cow.[(((((triple7) -> rule5)) -> rule3) OR ((((((triple3) -> rule3)) -> rule5)) -> rule3))] @3: The cow chases the mouse.[(((((((triple7) -> rule5)) -> rule3) triple1) -> rule1) OR ((((((((triple3) -> rule3)) -> rule5)) -> rule3) triple1) -> rule1))]
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
((triple7 triple2) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((((triple3) -> (rule3 % int2)) triple2) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse is not rough.
("mouse" "is" "rough" "-")
triple5
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
((triple3) -> (rule3 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int4