The cat is young. The dog needs the cat. The dog needs the lion. The dog sees the squirrel. The dog visits the lion. The lion sees the dog. The squirrel sees the cat. If something needs the dog then it sees the lion. If something sees the squirrel and the squirrel is young then the squirrel sees the dog. If something sees the dog then the dog sees the lion. If something sees the lion and it is red then the lion is red. If something is red and it sees the cat then the cat is blue. If something is red then it needs the dog. If the squirrel is green and the squirrel is rough then the squirrel is red. If something needs the lion and it sees the lion then it is red. If something visits the lion and it is young then it is rough.
The cat is young.
("cat" "is" "young" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something needs the dog then it sees the lion.
((("something" "needs" "dog" "+")) -> ("something" "sees" "lion" "+"))
If something sees the squirrel and the squirrel is young then the squirrel sees the dog.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "sees" "dog" "+"))
If something sees the dog then the dog sees the lion.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If something sees the lion and it is red then the lion is red.
((("something" "sees" "lion" "+") ("something" "is" "red" "+")) -> ("lion" "is" "red" "+"))
If something is red and it sees the cat then the cat is blue.
((("something" "is" "red" "+") ("something" "sees" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something is red then it needs the dog.
((("something" "is" "red" "+")) -> ("something" "needs" "dog" "+"))
If the squirrel is green and the squirrel is rough then the squirrel is red.
((("squirrel" "is" "green" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "is" "red" "+"))
If something needs the lion and it sees the lion then it is red.
((("something" "needs" "lion" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
If something visits the lion and it is young then it is rough.
((("something" "visits" "lion" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
The dog needs the lion.
True
1
proof
[(triple3)]
("dog" "needs" "lion" "+")
triple3
The dog does not need the cat.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cat" "-")
triple2
The dog sees the lion.
True
2
proof
[(((triple6) -> rule3))]
("dog" "sees" "lion" "+")
((triple6) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog does not see the lion.
False
2
inv-proof
[(((triple6) -> rule3))]
("dog" "sees" "lion" "-")
((triple6) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog is red.
True
4
proof
[(((triple3 ((triple6) -> rule3)) -> rule8))]
("dog" "is" "red" "+")
((triple3 ((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog is not red.
False
4
inv-proof
[(((triple3 ((triple6) -> rule3)) -> rule8))]
("dog" "is" "red" "-")
((triple3 ((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog needs the dog.
True
5
proof
[(((((triple3 ((triple6) -> rule3)) -> rule8)) -> rule6))]
("dog" "needs" "dog" "+")
((((triple3 ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The dog does not need the dog.
False
5
inv-proof
[(((((triple3 ((triple6) -> rule3)) -> rule8)) -> rule6))]
("dog" "needs" "dog" "-")
((((triple3 ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The lion needs the dog.
True
8
proof
[(((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6))]
("lion" "needs" "dog" "+")
((((((triple6) -> (rule3 % int4)) ((triple3 ((triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog sees the lion.
("dog" "sees" "lion" "+")
int4
The lion does not need the dog.
False
8
inv-proof
[(((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6))]
("lion" "needs" "dog" "-")
((((((triple6) -> (rule3 % int4)) ((triple3 ((triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog sees the lion.
("dog" "sees" "lion" "+")
int4
The lion sees the lion.
True
9
proof
[(((((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6)) -> rule1))]
("lion" "sees" "lion" "+")
((((((((triple6) -> (rule3 % int5)) ((triple3 ((triple6) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The dog sees the lion.
("dog" "sees" "lion" "+")
int5
The lion does not see the lion.
False
9
inv-proof
[(((((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6)) -> rule1))]
("lion" "sees" "lion" "-")
((((((((triple6) -> (rule3 % int5)) ((triple3 ((triple6) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The dog sees the lion.
("dog" "sees" "lion" "+")
int5
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "is" "rough" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("squirrel" "is" "rough" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "red" "-")
The cat is blue.
Unknown
rconc
[@2: The cat is blue.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("cat" "is" "blue" "+")
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel sees the lion.
Unknown
rconc
[@3: The squirrel sees the lion.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule7 <- FAIL)]]
("squirrel" "sees" "lion" "+")
The lion does not see the cat.
Unknown
inv-random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "-")
The lion needs the squirrel.
Unknown
random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The dog does not visit the cat.
Unknown
inv-random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat is young.[(triple1)] The dog needs the cat.[(triple2)] The dog needs the lion.[(triple3)] The dog sees the squirrel.[(triple4)] The dog visits the lion.[(triple5)] The lion sees the dog.[(triple6)] The squirrel sees the cat.[(triple7)] @1: The dog sees the lion.[(((triple6) -> rule3))] @2: The dog is red.[(((triple3 ((triple6) -> rule3)) -> rule8))] @3: The dog needs the dog.[(((((triple3 ((triple6) -> rule3)) -> rule8)) -> rule6))] The lion is red.[(((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4))] @4: The lion needs the dog.[(((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6))] @5: The lion sees the lion.[(((((((((triple6) -> rule3) ((triple3 ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule6)) -> rule1))]
The cat is young.
("cat" "is" "young" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
The lion sees the dog.
("lion" "sees" "dog" "+")
triple6
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple7
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple6) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((triple3 ((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple3 ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The lion is red.
("lion" "is" "red" "+")
((((triple6) -> (rule3 % int3)) ((triple3 ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
((((((triple6) -> (rule3 % int4)) ((triple3 ((triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog sees the lion.
("dog" "sees" "lion" "+")
int4
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((((triple6) -> (rule3 % int5)) ((triple3 ((triple6) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The dog sees the lion.
("dog" "sees" "lion" "+")
int5