The cat eats the cow. The cat eats the lion. The cat is green. The cat is not round. The cat does not see the cow. The cat sees the lion. The cat visits the cow. The cat visits the lion. The cow does not eat the cat. The cow is cold. The cow sees the lion. The cow visits the lion. The lion is blue. The lion sees the cat. The lion sees the cow. The lion visits the cat. If someone is cold and they do not eat the cow then they visit the lion. If someone sees the cat then they eat the lion. If someone visits the cow then the cow sees the cat. If someone eats the cow and they are not cold then the cow does not visit the lion. If the cow is green then the cow does not see the lion. If the cat eats the lion and the cat is blue then the lion is young.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat does not see the cow.
("cat" "sees" "cow" "-")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow does not eat the cat.
("cow" "eats" "cat" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone is cold and they do not eat the cow then they visit the lion.
((("someone" "is" "cold" "+") ("someone" "eats" "cow" "~")) -> ("someone" "visits" "lion" "+"))
If someone sees the cat then they eat the lion.
((("someone" "sees" "cat" "+")) -> ("someone" "eats" "lion" "+"))
If someone visits the cow then the cow sees the cat.
((("someone" "visits" "cow" "+")) -> ("cow" "sees" "cat" "+"))
If someone eats the cow and they are not cold then the cow does not visit the lion.
((("someone" "eats" "cow" "+") ("someone" "is" "cold" "~")) -> ("cow" "visits" "lion" "-"))
If the cow is green then the cow does not see the lion.
((("cow" "is" "green" "+")) -> ("cow" "sees" "lion" "-"))
If the cat eats the lion and the cat is blue then the lion is young.
((("cat" "eats" "lion" "+") ("cat" "is" "blue" "+")) -> ("lion" "is" "young" "+"))
The cow does not eat the cat.
True
1
proof
[(triple9)]
("cow" "eats" "cat" "-")
triple9
The cat is not green.
False
1
inv-proof
[(triple3)]
("cat" "is" "green" "-")
triple3
The lion eats the lion.
True
2
proof
[(((triple14) -> rule2))]
("lion" "eats" "lion" "+")
((triple14) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The cow does not see the cat.
False
2
inv-proof
[(((triple7) -> rule3))]
("cow" "sees" "cat" "-")
((triple7) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow eats the lion.
True
3
proof
[(((((triple7) -> rule3)) -> rule2))]
("cow" "eats" "lion" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow does not eat the lion.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2))]
("cow" "eats" "lion" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion is young.
Unknown
rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "young" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The cat does not see the cow.[(triple5)] The cat eats the cow.[(triple1)] The cat eats the lion.[(triple2)] The cat is green.[(triple3)] The cat is not round.[(triple4)] The cat sees the lion.[(triple6)] The cat visits the cow.[(triple7)] The cat visits the lion.[(triple8)] The cow does not eat the cat.[(triple9)] The cow is cold.[(triple10)] The cow sees the lion.[(triple11)] The cow visits the lion.[(triple12)] The lion is blue.[(triple13)] The lion sees the cat.[(triple14)] The lion sees the cow.[(triple15)] The lion visits the cat.[(triple16)] @1: The cow sees the cat.[(((triple7) -> rule3))] The lion eats the lion.[(((triple14) -> rule2))] @2: The cow eats the lion.[(((((triple7) -> rule3)) -> rule2))]
The cat does not see the cow.
("cat" "sees" "cow" "-")
triple5
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is not round.
("cat" "is" "round" "-")
triple4
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
The cat visits the cow.
("cat" "visits" "cow" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
triple8
The cow does not eat the cat.
("cow" "eats" "cat" "-")
triple9
The cow is cold.
("cow" "is" "cold" "+")
triple10
The cow sees the lion.
("cow" "sees" "lion" "+")
triple11
The cow visits the lion.
("cow" "visits" "lion" "+")
triple12
The lion is blue.
("lion" "is" "blue" "+")
triple13
The lion sees the cat.
("lion" "sees" "cat" "+")
triple14
The lion sees the cow.
("lion" "sees" "cow" "+")
triple15
The lion visits the cat.
("lion" "visits" "cat" "+")
triple16
The cow sees the cat.
("cow" "sees" "cat" "+")
((triple7) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple14) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2