The cat is big. The cat is blue. The cat is nice. The cat is rough. The cat is round. Nice, big things are rough. If the cat is round and the cat is nice then the cat is big.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
Nice, big things are rough.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If the cat is round and the cat is nice then the cat is big.
((("cat" "is" "round" "+") ("cat" "is" "nice" "+")) -> ("cat" "is" "big" "+"))
The cat is rough.
True
1
proof
[(triple4 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple5 triple3) -> rule2)) -> rule1))]
("cat" "is" "rough" "+")
triple4
((triple3 triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple3 ((triple5 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is not rough.
False
1
inv-proof
[(triple4 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple5 triple3) -> rule2)) -> rule1))]
("cat" "is" "rough" "-")
triple4
((triple3 triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple3 ((triple5 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is big.
("cat" "is" "big" "+")
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 needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is big.[(triple1 OR ((triple5 triple3) -> rule2))] The cat is blue.[(triple2)] The cat is nice.[(triple3)] The cat is rough.[(triple4 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple5 triple3) -> rule2)) -> rule1))] The cat is round.[(triple5)]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple5 triple3) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple3 triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple3 ((triple5 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is round.
("cat" "is" "round" "+")
triple5