The cow is nice. The cow likes the mouse. The mouse likes the cow. If something likes the mouse then it is green. If something sees the cow then the cow is green. If something is red then it visits the cow. If something visits the mouse then the mouse is green. If something is nice then it likes the mouse. If something likes the mouse then it visits the cow. If something is green then it sees the mouse. If something is nice then it visits the mouse.
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If something likes the mouse then it is green.
((("something" "likes" "mouse" "+")) -> ("something" "is" "green" "+"))
If something sees the cow then the cow is green.
((("something" "sees" "cow" "+")) -> ("cow" "is" "green" "+"))
If something is red then it visits the cow.
((("something" "is" "red" "+")) -> ("something" "visits" "cow" "+"))
If something visits the mouse then the mouse is green.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something is nice then it likes the mouse.
((("something" "is" "nice" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the mouse then it visits the cow.
((("something" "likes" "mouse" "+")) -> ("something" "visits" "cow" "+"))
If something is green then it sees the mouse.
((("something" "is" "green" "+")) -> ("something" "sees" "mouse" "+"))
If something is nice then it visits the mouse.
((("something" "is" "nice" "+")) -> ("something" "visits" "mouse" "+"))
The cow is nice.
True
1
proof
[(triple1)]
("cow" "is" "nice" "+")
triple1
The cow does not like the mouse.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule5))]
("cow" "likes" "mouse" "-")
triple2
((triple1) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the mouse.
True
2
proof
[(((triple1) -> rule8))]
("cow" "visits" "mouse" "+")
((triple1) -> (rule8 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((triple1) -> rule5)) -> rule6))]
("cow" "visits" "cow" "-")
((triple2) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow sees the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule7) OR ((((((triple1) -> rule5)) -> rule1)) -> rule7))]
("cow" "sees" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7) OR ((((((triple1) -> rule5)) -> rule1)) -> rule7))]
("cow" "sees" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The mouse sees the mouse.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule7))]
("mouse" "sees" "mouse" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The mouse does not see the mouse.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule7))]
("mouse" "sees" "mouse" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not visit the cow.
Unknown
inv-rconc
[@2: The mouse visits the cow.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("mouse" "visits" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow is nice.[(triple1)] The cow likes the mouse.[(triple2 OR ((triple1) -> rule5))] The mouse likes the cow.[(triple3)] @1: The cow is green.[(((triple2) -> rule1) OR ((((triple1) -> rule5)) -> rule1))] The cow visits the cow.[(((triple2) -> rule6) OR ((((triple1) -> rule5)) -> rule6))] The cow visits the mouse.[(((triple1) -> rule8))] @2: The cow sees the mouse.[(((((triple2) -> rule1)) -> rule7) OR ((((((triple1) -> rule5)) -> rule1)) -> rule7))] The mouse is green.[(((((triple1) -> rule8)) -> rule4))] @3: The mouse sees the mouse.[(((((((triple1) -> rule8)) -> rule4)) -> rule7))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
((triple1) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
((triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple2) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((triple1) -> (rule8 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3