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