The cat eats the dog. The cat eats the tiger. The cat is green. The cat is nice. The cat needs the dog. The cat visits the rabbit. The dog eats the tiger. The dog is green. The rabbit is kind. The rabbit is nice. The rabbit needs the tiger. The rabbit visits the cat. The rabbit visits the tiger. The tiger needs the rabbit. The tiger visits the rabbit. If the dog is blue and the dog is kind then the dog eats the tiger. If something visits the dog then it eats the tiger. If something is cold then it visits the dog. If something visits the rabbit then it is cold. If something is kind and nice then it visits the tiger. If something is green then it eats the tiger.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the dog is blue and the dog is kind then the dog eats the tiger.
((("dog" "is" "blue" "+") ("dog" "is" "kind" "+")) -> ("dog" "eats" "tiger" "+"))
If something visits the dog then it eats the tiger.
((("something" "visits" "dog" "+")) -> ("something" "eats" "tiger" "+"))
If something is cold then it visits the dog.
((("something" "is" "cold" "+")) -> ("something" "visits" "dog" "+"))
If something visits the rabbit then it is cold.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "cold" "+"))
If something is kind and nice then it visits the tiger.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "visits" "tiger" "+"))
If something is green then it eats the tiger.
((("something" "is" "green" "+")) -> ("something" "eats" "tiger" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple15)]
("tiger" "visits" "rabbit" "+")
triple15
The rabbit does not visit the cat.
False
1
inv-proof
[(triple12)]
("rabbit" "visits" "cat" "-")
triple12
The cat is cold.
True
2
proof
[(((triple6) -> rule4))]
("cat" "is" "cold" "+")
((triple6) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple6) -> rule4))]
("cat" "is" "cold" "-")
((triple6) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The tiger visits the dog.
True
3
proof
[(((((triple15) -> rule4)) -> rule3))]
("tiger" "visits" "dog" "+")
((((triple15) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cat does not visit the dog.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule3))]
("cat" "visits" "dog" "-")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The tiger eats the tiger.
True
4
proof
[(((((((triple15) -> rule4)) -> rule3)) -> rule2))]
("tiger" "eats" "tiger" "+")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger does not eat the tiger.
False
4
inv-proof
[(((((((triple15) -> rule4)) -> rule3)) -> rule2))]
("tiger" "eats" "tiger" "-")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "tiger" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "cold" "+")
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The dog does not eat the rabbit.
Unknown
inv-random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The tiger needs the dog.
Unknown
random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "+")
@0: The cat eats the dog.[(triple1)] The cat eats the tiger.[(triple2 OR ((triple3) -> rule6) OR ((((((triple6) -> rule4)) -> rule3)) -> rule2))] The cat is green.[(triple3)] The cat is nice.[(triple4)] The cat needs the dog.[(triple5)] The cat visits the rabbit.[(triple6)] The dog eats the tiger.[(triple7 OR ((triple8) -> rule6))] The dog is green.[(triple8)] The rabbit is kind.[(triple9)] The rabbit is nice.[(triple10)] The rabbit needs the tiger.[(triple11)] The rabbit visits the cat.[(triple12)] The rabbit visits the tiger.[(triple13 OR ((triple9 triple10) -> rule5))] The tiger needs the rabbit.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The cat is cold.[(((triple6) -> rule4))] The tiger is cold.[(((triple15) -> rule4))] @2: The cat visits the dog.[(((((triple6) -> rule4)) -> rule3))] The tiger visits the dog.[(((((triple15) -> rule4)) -> rule3))] @3: The tiger eats the tiger.[(((((((triple15) -> rule4)) -> rule3)) -> rule2))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
((triple3) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat needs the dog.
("cat" "needs" "dog" "+")
triple5
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple6
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple7
((triple8) -> (rule6 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple11
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple12
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple13
((triple9 triple10) -> (rule5 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The cat is cold.
("cat" "is" "cold" "+")
((triple6) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple15) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((((triple15) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple15) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3