The cat is green. The cat sees the cow. The cat visits the cow. The cow eats the cat. The cow is cold. The cow is green. The cow sees the cat. If something is green then it visits the cat. If something eats the cow and it is green then it is cold. If the cow is green then the cow is round. If something is cold and it visits the cow then it is nice. All round, nice things are cold. If something eats the cat then the cat eats the cow.
The cat is green.
("cat" "is" "green" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something is green then it visits the cat.
((("something" "is" "green" "+")) -> ("something" "visits" "cat" "+"))
If something eats the cow and it is green then it is cold.
((("something" "eats" "cow" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If the cow is green then the cow is round.
((("cow" "is" "green" "+")) -> ("cow" "is" "round" "+"))
If something is cold and it visits the cow then it is nice.
((("something" "is" "cold" "+") ("something" "visits" "cow" "+")) -> ("something" "is" "nice" "+"))
All round, nice things are cold.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something eats the cat then the cat eats the cow.
((("something" "eats" "cat" "+")) -> ("cat" "eats" "cow" "+"))
The cow sees the cat.
True
1
proof
[(triple7)]
("cow" "sees" "cat" "+")
triple7
The cow does not eat the cat.
False
1
inv-proof
[(triple4)]
("cow" "eats" "cat" "-")
triple4
The cow visits the cat.
True
2
proof
[(((triple6) -> rule1))]
("cow" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat does not eat the cow.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "eats" "cow" "-")
((triple4) -> (rule6 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is cold.
True
4
proof
[(((((triple4) -> rule6) triple1) -> rule2))]
("cat" "is" "cold" "+")
((((triple4) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is not cold.
False
4
inv-proof
[(((((triple4) -> rule6) triple1) -> rule2))]
("cat" "is" "cold" "-")
((((triple4) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is nice.
True
6
proof
[(((((((triple4) -> rule6) triple1) -> rule2) triple3) -> rule4))]
("cat" "is" "nice" "+")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cat is not nice.
False
6
inv-proof
[(((((((triple4) -> rule6) triple1) -> rule2) triple3) -> rule4))]
("cat" "is" "nice" "-")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "nice" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
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 sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is green.[(triple1)] The cat sees the cow.[(triple2)] The cat visits the cow.[(triple3)] The cow eats the cat.[(triple4)] The cow is cold.[(triple5)] The cow is green.[(triple6)] The cow sees the cat.[(triple7)] @1: The cat eats the cow.[(((triple4) -> rule6))] The cat visits the cat.[(((triple1) -> rule1))] The cow is round.[(((triple6) -> rule3))] The cow visits the cat.[(((triple6) -> rule1))] @2: The cat is cold.[(((((triple4) -> rule6) triple1) -> rule2))] @3: The cat is nice.[(((((((triple4) -> rule6) triple1) -> rule2) triple3) -> rule4))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple4) -> (rule6 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple6) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple4) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3