The cat chases the squirrel. The cat is blue. The dog is young. The dog needs the cat. The dog needs the squirrel. The dog needs the tiger. The squirrel is cold. The squirrel is green. The squirrel likes the cat. The tiger chases the cat. The tiger likes the dog. The tiger needs the dog. If something likes the dog and it chases the dog then the dog needs the cat. If something likes the tiger then the tiger likes the dog. If the tiger likes the dog and the tiger chases the squirrel then the squirrel chases the tiger. If something chases the squirrel and the squirrel chases the dog then the squirrel needs the tiger. If something likes the cat and the cat is cold then it chases the dog. If something chases the squirrel then it is cold. If something chases the tiger then the tiger is cold. If something is green and it needs the cat then it likes the cat.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something likes the dog and it chases the dog then the dog needs the cat.
((("something" "likes" "dog" "+") ("something" "chases" "dog" "+")) -> ("dog" "needs" "cat" "+"))
If something likes the tiger then the tiger likes the dog.
((("something" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If the tiger likes the dog and the tiger chases the squirrel then the squirrel chases the tiger.
((("tiger" "likes" "dog" "+") ("tiger" "chases" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If something chases the squirrel and the squirrel chases the dog then the squirrel needs the tiger.
((("something" "chases" "squirrel" "+") ("squirrel" "chases" "dog" "+")) -> ("squirrel" "needs" "tiger" "+"))
If something likes the cat and the cat is cold then it chases the dog.
((("something" "likes" "cat" "+") ("cat" "is" "cold" "+")) -> ("something" "chases" "dog" "+"))
If something chases the squirrel then it is cold.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If something chases the tiger then the tiger is cold.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something is green and it needs the cat then it likes the cat.
((("something" "is" "green" "+") ("something" "needs" "cat" "+")) -> ("something" "likes" "cat" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The dog does not need the cat.
False
1
inv-proof
[(triple4)]
("dog" "needs" "cat" "-")
triple4
The cat is cold.
True
2
proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "-")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel chases the dog.
True
4
proof
[(((triple9 ((triple1) -> rule6)) -> rule5))]
("squirrel" "chases" "dog" "+")
((triple9 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel does not chase the dog.
False
4
inv-proof
[(((triple9 ((triple1) -> rule6)) -> rule5))]
("squirrel" "chases" "dog" "-")
((triple9 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel needs the tiger.
True
6
proof
[(((triple1 ((triple9 ((triple1) -> rule6)) -> rule5)) -> rule4))]
("squirrel" "needs" "tiger" "+")
((triple1 ((triple9 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The squirrel does not need the tiger.
False
6
inv-proof
[(((triple1 ((triple9 ((triple1) -> rule6)) -> rule5)) -> rule4))]
("squirrel" "needs" "tiger" "-")
((triple1 ((triple9 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "likes" "cat" "-")
The dog chases the dog.
Unknown
rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("dog" "chases" "dog" "+")
The tiger is not cold.
Unknown
inv-rconc
[@2: The tiger is cold.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("tiger" "is" "cold" "-")
The cat chases the dog.
Unknown
rconc
[@2: The cat chases the dog.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("cat" "chases" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The cat needs the dog.
Unknown
random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The cat chases the squirrel.[(triple1)] The cat is blue.[(triple2)] The dog is young.[(triple3)] The dog needs the cat.[(triple4)] The dog needs the squirrel.[(triple5)] The dog needs the tiger.[(triple6)] The squirrel is cold.[(triple7)] The squirrel is green.[(triple8)] The squirrel likes the cat.[(triple9)] The tiger chases the cat.[(triple10)] The tiger likes the dog.[(triple11)] The tiger needs the dog.[(triple12)] @1: The cat is cold.[(((triple1) -> rule6))] @2: The squirrel chases the dog.[(((triple9 ((triple1) -> rule6)) -> rule5))] @3: The squirrel needs the tiger.[(((triple1 ((triple9 ((triple1) -> rule6)) -> rule5)) -> rule4))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog needs the cat.
("dog" "needs" "cat" "+")
triple4
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple11
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple12
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
((triple9 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
((triple1 ((triple9 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3