The dog sees the lion. The dog sees the squirrel. The dog visits the squirrel. The lion chases the dog. The lion is big. The lion is rough. The lion sees the dog. The lion sees the squirrel. The lion visits the squirrel. The squirrel visits the lion. All rough things are big. If the lion visits the squirrel then the lion visits the dog. If something visits the lion then the lion visits the dog. If something chases the squirrel and it visits the dog then it is cold. If something visits the dog and it sees the squirrel then it is red. If something is big then it visits the squirrel.
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If the lion visits the squirrel then the lion visits the dog.
((("lion" "visits" "squirrel" "+")) -> ("lion" "visits" "dog" "+"))
If something visits the lion then the lion visits the dog.
((("something" "visits" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If something chases the squirrel and it visits the dog then it is cold.
((("something" "chases" "squirrel" "+") ("something" "visits" "dog" "+")) -> ("something" "is" "cold" "+"))
If something visits the dog and it sees the squirrel then it is red.
((("something" "visits" "dog" "+") ("something" "sees" "squirrel" "+")) -> ("something" "is" "red" "+"))
If something is big then it visits the squirrel.
((("something" "is" "big" "+")) -> ("something" "visits" "squirrel" "+"))
The squirrel visits the lion.
True
1
proof
[(triple10)]
("squirrel" "visits" "lion" "+")
triple10
The dog does not visit the squirrel.
False
1
inv-proof
[(triple3)]
("dog" "visits" "squirrel" "-")
triple3
The lion visits the dog.
True
2
proof
[(((triple10) -> rule3) OR ((triple9) -> rule2) OR ((((triple5) -> rule6)) -> rule2) OR ((((((triple6) -> rule1)) -> rule6)) -> rule2))]
("lion" "visits" "dog" "+")
((triple10) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion does not visit the dog.
False
2
inv-proof
[(((triple10) -> rule3) OR ((triple9) -> rule2) OR ((((triple5) -> rule6)) -> rule2) OR ((((((triple6) -> rule1)) -> rule6)) -> rule2))]
("lion" "visits" "dog" "-")
((triple10) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is red.
True
4
proof
[(((((triple10) -> rule3) triple8) -> rule5) OR ((((triple9) -> rule2) triple8) -> rule5) OR ((((((triple5) -> rule6)) -> rule2) triple8) -> rule5) OR ((((((((triple6) -> rule1)) -> rule6)) -> rule2) triple8) -> rule5))]
("lion" "is" "red" "+")
((((triple10) -> (rule3 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple9) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((((((((triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion is not red.
False
4
inv-proof
[(((((triple10) -> rule3) triple8) -> rule5) OR ((((triple9) -> rule2) triple8) -> rule5) OR ((((((triple5) -> rule6)) -> rule2) triple8) -> rule5) OR ((((((((triple6) -> rule1)) -> rule6)) -> rule2) triple8) -> rule5))]
("lion" "is" "red" "-")
((((triple10) -> (rule3 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple9) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((((((((triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "cold" "-")
The squirrel is red.
Unknown
rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "red" "+")
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "red" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not see the lion.
Unknown
inv-random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The dog sees the lion.[(triple1)] The dog sees the squirrel.[(triple2)] The dog visits the squirrel.[(triple3)] The lion chases the dog.[(triple4)] The lion is big.[(triple5 OR ((triple6) -> rule1))] The lion is rough.[(triple6)] The lion sees the dog.[(triple7)] The lion sees the squirrel.[(triple8)] The lion visits the squirrel.[(triple9 OR ((triple5) -> rule6) OR ((((triple6) -> rule1)) -> rule6))] The squirrel visits the lion.[(triple10)] @1: The lion visits the dog.[(((triple10) -> rule3) OR ((triple9) -> rule2) OR ((((triple5) -> rule6)) -> rule2) OR ((((((triple6) -> rule1)) -> rule6)) -> rule2))] @2: The lion is red.[(((((triple10) -> rule3) triple8) -> rule5) OR ((((triple9) -> rule2) triple8) -> rule5) OR ((((((triple5) -> rule6)) -> rule2) triple8) -> rule5) OR ((((((((triple6) -> rule1)) -> rule6)) -> rule2) triple8) -> rule5))]
The dog sees the lion.
("dog" "sees" "lion" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple3
The lion chases the dog.
("lion" "chases" "dog" "+")
triple4
The lion is big.
("lion" "is" "big" "+")
triple5
((triple6) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion sees the dog.
("lion" "sees" "dog" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple8
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple9
((triple5) -> (rule6 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple10) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is red.
("lion" "is" "red" "+")
((((triple10) -> (rule3 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple9) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((((((((triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4