The cat is big. The cat is kind. The cat is red. The cat is rough. The cat is young. If the cat is kind then the cat is red. If the cat is red and the cat is young then the cat is big. If the cat is kind and the cat is red then the cat is big. If someone is red and young then they are kind. If the cat is big and the cat is rough then the cat is young. Big, rough people are young.
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
If the cat is kind then the cat is red.
((("cat" "is" "kind" "+")) -> ("cat" "is" "red" "+"))
If the cat is red and the cat is young then the cat is big.
((("cat" "is" "red" "+") ("cat" "is" "young" "+")) -> ("cat" "is" "big" "+"))
If the cat is kind and the cat is red then the cat is big.
((("cat" "is" "kind" "+") ("cat" "is" "red" "+")) -> ("cat" "is" "big" "+"))
If someone is red and young then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If the cat is big and the cat is rough then the cat is young.
((("cat" "is" "big" "+") ("cat" "is" "rough" "+")) -> ("cat" "is" "young" "+"))
Big, rough people are young.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
The cat is kind.
True
1
proof
[(triple2 OR ((triple3 triple5) -> rule4) OR ((triple3 ((triple1 triple4) -> rule5)) -> rule4) OR ((triple3 ((triple1 triple4) -> rule6)) -> rule4))]
("cat" "is" "kind" "+")
triple2
((triple3 triple5) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3 ((triple1 triple4) -> (rule5 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple3 ((triple1 triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is not kind.
False
1
inv-proof
[(triple2 OR ((triple3 triple5) -> rule4) OR ((triple3 ((triple1 triple4) -> rule5)) -> rule4) OR ((triple3 ((triple1 triple4) -> rule6)) -> rule4))]
("cat" "is" "kind" "-")
triple2
((triple3 triple5) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3 ((triple1 triple4) -> (rule5 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple3 ((triple1 triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is big.[(triple1 OR ((triple2 triple3) -> rule3) OR ((triple3 triple5) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule1) triple5) -> rule2) OR ((((triple3 triple5) -> rule4) triple3) -> rule3) OR ((((triple3 triple5) -> rule4) ((triple2) -> rule1)) -> rule3))] The cat is kind.[(triple2 OR ((triple3 triple5) -> rule4) OR ((triple3 ((triple1 triple4) -> rule5)) -> rule4) OR ((triple3 ((triple1 triple4) -> rule6)) -> rule4))] The cat is red.[(triple3 OR ((triple2) -> rule1))] The cat is rough.[(triple4)] The cat is young.[(triple5 OR ((triple1 triple4) -> rule5) OR ((triple1 triple4) -> rule6) OR ((((triple2 triple3) -> rule3) triple4) -> rule5) OR ((((triple2 triple3) -> rule3) triple4) -> rule6) OR ((((triple2 ((triple2) -> rule1)) -> rule3) triple4) -> rule5) OR ((((triple2 ((triple2) -> rule1)) -> rule3) triple4) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple3 triple5) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple2) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple3 triple5) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple3 triple5) -> (rule4 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
triple2
((triple3 triple5) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3 ((triple1 triple4) -> (rule5 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((triple3 ((triple1 triple4) -> (rule6 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is red.
("cat" "is" "red" "+")
triple3
((triple2) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
((triple1 triple4) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple1 triple4) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple2 triple3) -> (rule3 % int2)) triple4) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple2 triple3) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3