The cat is red. The cat is rough. The cat is round. Young things are rough. If something is round then it is green. If something is rough and red then it is young. All young, rough things are red. All round, red things are rough. All young things are green. Red things are rough. All red things are young.
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is rough and red then it is young.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All young, rough things are red.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All round, red things are rough.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
The cat is round.
True
1
proof
[(triple3)]
("cat" "is" "round" "+")
triple3
The cat is not rough.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule7) OR ((triple3 triple1) -> rule5) OR ((((triple1) -> rule8)) -> rule1))]
("cat" "is" "rough" "-")
triple2
((triple1) -> (rule7 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is red.[(triple1)] The cat is rough.[(triple2 OR ((triple1) -> rule7) OR ((triple3 triple1) -> rule5) OR ((((triple1) -> rule8)) -> rule1))] The cat is round.[(triple3)] @1: The cat is green.[(((triple3) -> rule2) OR ((((triple1) -> rule8)) -> rule6) OR ((((triple2 triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule7) triple1) -> rule3)) -> rule6) OR ((((((triple3 triple1) -> rule5) triple1) -> rule3)) -> rule6))] The cat is young.[(((triple1) -> rule8) OR ((triple2 triple1) -> rule3) OR ((((triple1) -> rule7) triple1) -> rule3) OR ((((triple3 triple1) -> rule5) triple1) -> rule3))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
((triple1) -> (rule7 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((((triple3 triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple2 triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple1) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple3 triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2