The cat chases the tiger. The cat is blue. The cat is not cold. The cat is green. The cat is nice. The cat is round. The cat needs the tiger. The cat visits the tiger. The tiger chases the cat. The tiger is blue. The tiger is cold. The tiger is green. The tiger is round. The tiger needs the cat. The tiger visits the cat. If something is green then it visits the cat. If the tiger is nice then the tiger needs the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something is green then it visits the cat.
((("something" "is" "green" "+")) -> ("something" "visits" "cat" "+"))
If the tiger is nice then the tiger needs the cat.
((("tiger" "is" "nice" "+")) -> ("tiger" "needs" "cat" "+"))
The tiger chases the cat.
True
1
proof
[(triple9)]
("tiger" "chases" "cat" "+")
triple9
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The cat visits the cat.
True
2
proof
[(((triple4) -> rule1))]
("cat" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "visits" "cat" "-")
((triple4) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
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 chases the tiger.[(triple1)] The cat is blue.[(triple2)] The cat is green.[(triple4)] The cat is nice.[(triple5)] The cat is not cold.[(triple3)] The cat is round.[(triple6)] The cat needs the tiger.[(triple7)] The cat visits the tiger.[(triple8)] The tiger chases the cat.[(triple9)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is green.[(triple12)] The tiger is round.[(triple13)] The tiger needs the cat.[(triple14)] The tiger visits the cat.[(triple15 OR ((triple12) -> rule1))] @1: The cat visits the cat.[(((triple4) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is not cold.
("cat" "is" "cold" "-")
triple3
The cat is round.
("cat" "is" "round" "+")
triple6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple8
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
((triple12) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1