The cat needs the dog. The dog is green. The dog visits the cat. The dog visits the tiger. The squirrel is red. The squirrel visits the dog. The tiger is rough. The tiger likes the cat. The tiger needs the dog. The tiger visits the cat. All rough people are cold. If someone likes the dog then the dog needs the tiger. If someone is cold then they visit the squirrel. If someone needs the squirrel and the squirrel likes the tiger then they need the cat. If someone is rough and they visit the squirrel then the squirrel is rough.
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the dog then the dog needs the tiger.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If someone is cold then they visit the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone needs the squirrel and the squirrel likes the tiger then they need the cat.
((("someone" "needs" "squirrel" "+") ("squirrel" "likes" "tiger" "+")) -> ("someone" "needs" "cat" "+"))
If someone is rough and they visit the squirrel then the squirrel is rough.
((("someone" "is" "rough" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The cat does not need the dog.
False
1
inv-proof
[(triple1)]
("cat" "needs" "dog" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "is" "cold" "+")
((triple7) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "is" "cold" "-")
((triple7) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the squirrel.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("tiger" "visits" "squirrel" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger does not visit the squirrel.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3))]
("tiger" "visits" "squirrel" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The squirrel is rough.
True
5
proof
[(((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5))]
("squirrel" "is" "rough" "+")
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The squirrel is not rough.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5))]
("squirrel" "is" "rough" "-")
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The squirrel is cold.
True
6
proof
[(((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1))]
("squirrel" "is" "cold" "+")
((((triple7 ((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The squirrel is not cold.
False
6
inv-proof
[(((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1))]
("squirrel" "is" "cold" "-")
((((triple7 ((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The squirrel visits the squirrel.
True
7
proof
[(((((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "visits" "squirrel" "+")
((((((triple7 ((((triple7) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
int5
The squirrel does not visit the squirrel.
False
7
inv-proof
[(((((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((((((triple7 ((((triple7) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
int5
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "cat" "+")
The squirrel does not need the cat.
Unknown
inv-rconc
[@1: The squirrel needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "cat" "-")
The dog visits the squirrel.
Unknown
rconc
[@2: The dog visits the squirrel.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "visits" "squirrel" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "-")
The dog needs the tiger.
Unknown
rconc
[@1: The dog needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "tiger" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The cat needs the dog.[(triple1)] The dog is green.[(triple2)] The dog visits the cat.[(triple3)] The dog visits the tiger.[(triple4)] The squirrel is red.[(triple5)] The squirrel visits the dog.[(triple6)] The tiger is rough.[(triple7)] The tiger likes the cat.[(triple8)] The tiger needs the dog.[(triple9)] The tiger visits the cat.[(triple10)] @1: The tiger is cold.[(((triple7) -> rule1))] @2: The tiger visits the squirrel.[(((((triple7) -> rule1)) -> rule3))] @3: The squirrel is rough.[(((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5))] @4: The squirrel is cold.[(((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1))] @5: The squirrel visits the squirrel.[(((((((triple7 ((((triple7) -> rule1)) -> rule3)) -> rule5)) -> rule1)) -> rule3))]
The cat needs the dog.
("cat" "needs" "dog" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog visits the cat.
("dog" "visits" "cat" "+")
triple3
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple4
The squirrel is red.
("squirrel" "is" "red" "+")
triple5
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple8
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
((triple7) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple7 ((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((((triple7 ((((triple7) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
int5