The cow is cold. The squirrel visits the cow. If something sees the cow and the cow sees the squirrel then the squirrel sees the cow. If something visits the cow then the cow eats the squirrel. If something eats the squirrel and the squirrel sees the cow then it visits the cow. If something is cold then it eats the squirrel. If something eats the squirrel and it is not nice then the squirrel does not visit the cow. If the squirrel is rough then the squirrel does not visit the cow. If the cow eats the squirrel then the cow visits the squirrel. If something visits the squirrel then it is round.
The cow is cold.
("cow" "is" "cold" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something sees the cow and the cow sees the squirrel then the squirrel sees the cow.
((("something" "sees" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
If something visits the cow then the cow eats the squirrel.
((("something" "visits" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If something eats the squirrel and the squirrel sees the cow then it visits the cow.
((("something" "eats" "squirrel" "+") ("squirrel" "sees" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something is cold then it eats the squirrel.
((("something" "is" "cold" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the squirrel and it is not nice then the squirrel does not visit the cow.
((("something" "eats" "squirrel" "+") ("something" "is" "nice" "~")) -> ("squirrel" "visits" "cow" "-"))
If the squirrel is rough then the squirrel does not visit the cow.
((("squirrel" "is" "rough" "+")) -> ("squirrel" "visits" "cow" "-"))
If the cow eats the squirrel then the cow visits the squirrel.
((("cow" "eats" "squirrel" "+")) -> ("cow" "visits" "squirrel" "+"))
If something visits the squirrel then it is round.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "round" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The squirrel does not visit the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "visits" "cow" "-")
triple2
The cow eats the squirrel.
True
2
proof
[(((triple1) -> rule4) OR ((triple2) -> rule2))]
("cow" "eats" "squirrel" "+")
((triple1) -> (rule4 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple2) -> rule2))]
("cow" "eats" "squirrel" "-")
((triple1) -> (rule4 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow visits the squirrel.
True
3
proof
[(((((triple1) -> rule4)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))]
("cow" "visits" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow does not visit the squirrel.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))]
("cow" "visits" "squirrel" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel sees the cow.
Unknown
rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "cow" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "round" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The cow is cold.[(triple1)] The squirrel visits the cow.[(triple2)] @1: The cow eats the squirrel.[(((triple1) -> rule4) OR ((triple2) -> rule2))] @2: The cow visits the squirrel.[(((((triple1) -> rule4)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))] @3: The cow is round.[(((((((triple1) -> rule4)) -> rule7)) -> rule8) OR ((((((triple2) -> rule2)) -> rule7)) -> rule8))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((triple1) -> (rule4 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int3
((((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int3