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