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