The cat is cold. The cat is young. The cat likes the lion. The cat sees the rabbit. The lion is blue. The lion is young. The lion likes the rabbit. The lion sees the rabbit. The lion visits the mouse. The mouse is young. The mouse does not like the cat. The mouse sees the cat. The rabbit does not like the mouse. The rabbit sees the lion. The rabbit visits the lion. The rabbit does not visit the mouse. If the lion visits the cat and the cat is cold then the cat is big. If something sees the rabbit and it is not green then the rabbit sees the cat. If something visits the lion then the lion sees the mouse. If something is big then it visits the cat. If something visits the lion and the lion sees the mouse then the lion is big. If something is cold then it visits the rabbit. If something visits the cat and the cat likes the rabbit then it likes the mouse. If something sees the lion and it is blue then it sees the rabbit.
The cat is cold.
("cat" "is" "cold" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
If the lion visits the cat and the cat is cold then the cat is big.
((("lion" "visits" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "is" "big" "+"))
If something sees the rabbit and it is not green then the rabbit sees the cat.
((("something" "sees" "rabbit" "+") ("something" "is" "green" "~")) -> ("rabbit" "sees" "cat" "+"))
If something visits the lion then the lion sees the mouse.
((("something" "visits" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something is big then it visits the cat.
((("something" "is" "big" "+")) -> ("something" "visits" "cat" "+"))
If something visits the lion and the lion sees the mouse then the lion is big.
((("something" "visits" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("lion" "is" "big" "+"))
If something is cold then it visits the rabbit.
((("something" "is" "cold" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the cat and the cat likes the rabbit then it likes the mouse.
((("something" "visits" "cat" "+") ("cat" "likes" "rabbit" "+")) -> ("something" "likes" "mouse" "+"))
If something sees the lion and it is blue then it sees the rabbit.
((("something" "sees" "lion" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "rabbit" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The mouse likes the cat.
False
1
inv-proof
[(triple11)]
("mouse" "likes" "cat" "+")
triple11
The cat visits the rabbit.
True
2
proof
[(((triple1) -> rule6))]
("cat" "visits" "rabbit" "+")
((triple1) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The lion does not see the mouse.
False
2
inv-proof
[(((triple15) -> rule3))]
("lion" "sees" "mouse" "-")
((triple15) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion is big.
True
4
proof
[(((triple15 ((triple15) -> rule3)) -> rule5))]
("lion" "is" "big" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion is not big.
False
4
inv-proof
[(((triple15 ((triple15) -> rule3)) -> rule5))]
("lion" "is" "big" "-")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion visits the cat.
True
5
proof
[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4))]
("lion" "visits" "cat" "+")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The lion does not visit the cat.
False
5
inv-proof
[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4))]
("lion" "visits" "cat" "-")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The cat is big.
True
7
proof
[(((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1))]
("cat" "is" "big" "+")
((((((triple15 ((triple15) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int4
The cat is not big.
False
7
inv-proof
[(((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1))]
("cat" "is" "big" "-")
((((((triple15 ((triple15) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int4
The cat visits the cat.
True
8
proof
[(((((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1)) -> rule4))]
("cat" "visits" "cat" "+")
((((((((triple15 ((triple15) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int5
The cat does not visit the cat.
False
8
inv-proof
[(((((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1)) -> rule4))]
("cat" "visits" "cat" "-")
((((((((triple15 ((triple15) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int5
The mouse does not see the rabbit.
Unknown
inv-rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The mouse visits the rabbit.
Unknown
rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "rabbit" "+")
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit sees the cat.
Unknown
rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "cat" "+")
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "cat" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The rabbit does not like the cat.
Unknown
inv-random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The cat visits the lion.
Unknown
random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "+")
@0: The cat is cold.[(triple1)] The cat is young.[(triple2)] The cat likes the lion.[(triple3)] The cat sees the rabbit.[(triple4)] The lion is blue.[(triple5)] The lion is young.[(triple6)] The lion likes the rabbit.[(triple7)] The lion sees the rabbit.[(triple8)] The lion visits the mouse.[(triple9)] The mouse does not like the cat.[(triple11)] The mouse is young.[(triple10)] The mouse sees the cat.[(triple12)] The rabbit does not like the mouse.[(triple13)] The rabbit does not visit the mouse.[(triple16)] The rabbit sees the lion.[(triple14)] The rabbit visits the lion.[(triple15)] @1: The cat visits the rabbit.[(((triple1) -> rule6))] The lion sees the mouse.[(((triple15) -> rule3))] @2: The lion is big.[(((triple15 ((triple15) -> rule3)) -> rule5))] @3: The lion visits the cat.[(((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4))] @4: The cat is big.[(((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1))] @5: The cat visits the cat.[(((((((((triple15 ((triple15) -> rule3)) -> rule5)) -> rule4) triple1) -> rule1)) -> rule4))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple7
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple9
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple13
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple16
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple1) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((triple15) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
((((triple15 ((triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The cat is big.
("cat" "is" "big" "+")
((((((triple15 ((triple15) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int4
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((((triple15 ((triple15) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int5