The cat chases the tiger. The cat is big. The cat is nice. The cat needs the tiger. The cat sees the tiger. The tiger is blue. The tiger is cold. The tiger is young. The tiger does not need the cat. The tiger sees the cat. If something is nice and it needs the cat then it does not see the cat. If something chases the tiger then it is blue. If something chases the tiger and the tiger needs the cat then the tiger is young. If something sees the tiger and it is blue then it is young. If something is young then it chases the cat. If something needs the cat and the cat needs the tiger then it chases the cat. If something is big and it sees the cat then it does not need the tiger. If something needs the tiger and it does not need the cat then the tiger does not chase the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is nice and it needs the cat then it does not see the cat.
((("something" "is" "nice" "+") ("something" "needs" "cat" "+")) -> ("something" "sees" "cat" "-"))
If something chases the tiger then it is blue.
((("something" "chases" "tiger" "+")) -> ("something" "is" "blue" "+"))
If something chases the tiger and the tiger needs the cat then the tiger is young.
((("something" "chases" "tiger" "+") ("tiger" "needs" "cat" "+")) -> ("tiger" "is" "young" "+"))
If something sees the tiger and it is blue then it is young.
((("something" "sees" "tiger" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is young then it chases the cat.
((("something" "is" "young" "+")) -> ("something" "chases" "cat" "+"))
If something needs the cat and the cat needs the tiger then it chases the cat.
((("something" "needs" "cat" "+") ("cat" "needs" "tiger" "+")) -> ("something" "chases" "cat" "+"))
If something is big and it sees the cat then it does not need the tiger.
((("something" "is" "big" "+") ("something" "sees" "cat" "+")) -> ("something" "needs" "tiger" "-"))
If something needs the tiger and it does not need the cat then the tiger does not chase the cat.
((("something" "needs" "tiger" "+") ("something" "needs" "cat" "~")) -> ("tiger" "chases" "cat" "-"))
The tiger sees the cat.
True
1
proof
[(triple10)]
("tiger" "sees" "cat" "+")
triple10
The tiger does not see the cat.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "cat" "-")
triple10
The cat is blue.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple8) -> rule5))]
("tiger" "chases" "cat" "-")
((triple8) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat is young.
True
4
proof
[(((triple5 ((triple1) -> rule2)) -> rule4))]
("cat" "is" "young" "+")
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not young.
False
4
inv-proof
[(((triple5 ((triple1) -> rule2)) -> rule4))]
("cat" "is" "young" "-")
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat chases the cat.
True
5
proof
[(((((triple5 ((triple1) -> rule2)) -> rule4)) -> rule5))]
("cat" "chases" "cat" "+")
((((triple5 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat does not chase the cat.
False
5
inv-proof
[(((((triple5 ((triple1) -> rule2)) -> rule4)) -> rule5))]
("cat" "chases" "cat" "-")
((((triple5 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat is big.[(triple2)] The cat is nice.[(triple3)] The cat needs the tiger.[(triple4)] The cat sees the tiger.[(triple5)] The tiger does not need the cat.[(triple9)] The tiger is blue.[(triple6)] The tiger is cold.[(triple7)] The tiger is young.[(triple8)] The tiger sees the cat.[(triple10)] @1: The cat is blue.[(((triple1) -> rule2))] The tiger chases the cat.[(((triple8) -> rule5))] @2: The cat is young.[(((triple5 ((triple1) -> rule2)) -> rule4))] @3: The cat chases the cat.[(((((triple5 ((triple1) -> rule2)) -> rule4)) -> rule5))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The cat is blue.
("cat" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple8) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple5 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple5 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3