The cat does not eat the tiger. The cat is big. The cat is cold. The cat is kind. The cat is rough. The cat needs the tiger. The cat visits the tiger. The tiger eats the cat. The tiger is big. The tiger is not cold. The tiger is kind. The tiger is nice. The tiger is rough. The tiger does not need the cat. The tiger visits the cat. If the tiger visits the cat and the tiger is kind then the tiger is big. If someone is cold then they are nice. If someone is nice then they do not need the cat.
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the tiger visits the cat and the tiger is kind then the tiger is big.
((("tiger" "visits" "cat" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "is" "big" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they do not need the cat.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cat" "-"))
The cat is kind.
True
1
proof
[(triple4)]
("cat" "is" "kind" "+")
triple4
The tiger does not visit the cat.
False
1
inv-proof
[(triple15)]
("tiger" "visits" "cat" "-")
triple15
The cat is nice.
True
2
proof
[(((triple3) -> rule2))]
("cat" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "is" "nice" "-")
((triple3) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat does not need the cat.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("cat" "needs" "cat" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat needs the cat.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("cat" "needs" "cat" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cat does not eat the tiger.[(triple1)] The cat is big.[(triple2)] The cat is cold.[(triple3)] The cat is kind.[(triple4)] The cat is rough.[(triple5)] The cat needs the tiger.[(triple6)] The cat visits the tiger.[(triple7)] The tiger does not need the cat.[(triple14 OR ((triple12) -> rule3))] The tiger eats the cat.[(triple8)] The tiger is big.[(triple9 OR ((triple15 triple11) -> rule1))] The tiger is kind.[(triple11)] The tiger is nice.[(triple12)] The tiger is not cold.[(triple10)] The tiger is rough.[(triple13)] The tiger visits the cat.[(triple15)] @1: The cat is nice.[(((triple3) -> rule2))] @2: The cat does not need the cat.[(((((triple3) -> rule2)) -> rule3))]
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple6
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple7
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple14
((triple12) -> (rule3 % int1))
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
((triple15 triple11) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is not cold.
("tiger" "is" "cold" "-")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The cat is nice.
("cat" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat does not need the cat.
("cat" "needs" "cat" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2