The cat is cold. The cat is red. The cat is rough. The cat is round. The cat is young. If something is red then it is rough. If something is young and not cold then it is not rough. Cold things are rough. All round, cold things are young. If the cat is young then the cat is red. If the cat is round then the cat is rough.
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is young and not cold then it is not rough.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "-"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All round, cold things are young.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If the cat is young then the cat is red.
((("cat" "is" "young" "+")) -> ("cat" "is" "red" "+"))
If the cat is round then the cat is rough.
((("cat" "is" "round" "+")) -> ("cat" "is" "rough" "+"))
The cat is young.
True
1
proof
[(triple5 OR ((triple4 triple1) -> rule4))]
("cat" "is" "young" "+")
triple5
((triple4 triple1) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not rough.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule3) OR ((triple2) -> rule1) OR ((triple4) -> rule6) OR ((((triple5) -> rule5)) -> rule1) OR ((((((triple4 triple1) -> rule4)) -> rule5)) -> rule1))]
("cat" "is" "rough" "-")
triple3
((triple1) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple2) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple4) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple4 triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is cold.[(triple1)] The cat is red.[(triple2 OR ((triple5) -> rule5) OR ((((triple4 triple1) -> rule4)) -> rule5))] The cat is rough.[(triple3 OR ((triple1) -> rule3) OR ((triple2) -> rule1) OR ((triple4) -> rule6) OR ((((triple5) -> rule5)) -> rule1) OR ((((((triple4 triple1) -> rule4)) -> rule5)) -> rule1))] The cat is round.[(triple4)] The cat is young.[(triple5 OR ((triple4 triple1) -> rule4))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
((triple5) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple4 triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple3
((triple1) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple2) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple4) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple4 triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
((triple4 triple1) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1