The cat is big. The cat is nice. The cat is round. The cat needs the squirrel. The lion is cold. The lion is nice. The lion is red. The lion is round. The lion does not need the squirrel. The lion visits the cat. The lion visits the squirrel. The squirrel is not nice. The squirrel needs the cat. The squirrel needs the lion. The squirrel sees the cat. The squirrel sees the lion. If something sees the squirrel then it sees the lion. If something sees the lion and it is round then the lion is big. If something is big then it sees the squirrel. If something needs the cat and the cat is cold then the cat needs the lion. If something sees the lion and it does not need the squirrel then it does not need the cat. If something needs the cat then it sees the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the squirrel then it sees the lion.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "lion" "+"))
If something sees the lion and it is round then the lion is big.
((("something" "sees" "lion" "+") ("something" "is" "round" "+")) -> ("lion" "is" "big" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something needs the cat and the cat is cold then the cat needs the lion.
((("something" "needs" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "needs" "lion" "+"))
If something sees the lion and it does not need the squirrel then it does not need the cat.
((("something" "sees" "lion" "+") ("something" "needs" "squirrel" "~")) -> ("something" "needs" "cat" "-"))
If something needs the cat then it sees the cat.
((("something" "needs" "cat" "+")) -> ("something" "sees" "cat" "+"))
The squirrel needs the cat.
True
1
proof
[(triple13)]
("squirrel" "needs" "cat" "+")
triple13
The lion needs the squirrel.
False
1
inv-proof
[(triple9)]
("lion" "needs" "squirrel" "+")
triple9
The cat sees the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("cat" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "sees" "squirrel" "-")
((triple1) -> (rule3 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat sees the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("cat" "sees" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat does not see the lion.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cat" "sees" "lion" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The lion is big.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple3) -> rule2))]
("lion" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int3
The lion is not big.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple3) -> rule2))]
("lion" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int3
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The lion does not see the cat.
Unknown
inv-rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "cat" "-")
The cat needs the lion.
Unknown
rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "lion" "+")
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is big.[(triple1)] The cat is nice.[(triple2)] The cat is round.[(triple3)] The cat needs the squirrel.[(triple4)] The lion does not need the squirrel.[(triple9)] The lion is cold.[(triple5)] The lion is nice.[(triple6)] The lion is red.[(triple7)] The lion is round.[(triple8)] The lion visits the cat.[(triple10)] The lion visits the squirrel.[(triple11)] The squirrel is not nice.[(triple12)] The squirrel needs the cat.[(triple13)] The squirrel needs the lion.[(triple14)] The squirrel sees the cat.[(triple15 OR ((triple13) -> rule6))] The squirrel sees the lion.[(triple16)] @1: The cat sees the squirrel.[(((triple1) -> rule3))] @2: The cat sees the lion.[(((((triple1) -> rule3)) -> rule1))] @3: The lion is big.[(((((((triple1) -> rule3)) -> rule1) triple3) -> rule2))] @4: The lion sees the squirrel.[(((((((((triple1) -> rule3)) -> rule1) triple3) -> rule2)) -> rule3))] @5: The lion sees the lion.[(((((((((((triple1) -> rule3)) -> rule1) triple3) -> rule2)) -> rule3)) -> rule1))] @6: The lion does not need the cat.[(((((((((((((triple1) -> rule3)) -> rule1) triple3) -> rule2)) -> rule3)) -> rule1) triple9) -> rule5))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple4
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion is red.
("lion" "is" "red" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
The lion visits the cat.
("lion" "visits" "cat" "+")
triple10
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple11
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple12
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple13
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple14
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple15
((triple13) -> (rule6 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple16
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat sees the lion.
("cat" "sees" "lion" "+")
int3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int4
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule1 % int4)) triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The cat sees the lion.
("cat" "sees" "lion" "+")
int4
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int5
The lion does not need the cat.
("lion" "needs" "cat" "-")
((((((((((((triple1) -> (rule3 % int6))) -> (rule1 % int5)) triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule5 % int1))
The lion does not need the cat.
("lion" "needs" "cat" "-")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The cat sees the lion.
("cat" "sees" "lion" "+")
int5
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int6