Charlie is cold. Charlie is green. Charlie is quiet. Charlie is red. Charlie is rough. Dave is big. Dave is cold. Dave is quiet. Dave is red. Dave is young. Cold things are young. If something is young and big then it is quiet. If something is red and cold then it is young.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is young and big then it is quiet.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is red and cold then it is young.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple10 OR ((triple7) -> rule1) OR ((triple9 triple7) -> rule3))]
("Dave" "is" "young" "+")
triple10
((triple7) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple9 triple7) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Charlie is young.
True
2
proof
[(((triple1) -> rule1) OR ((triple4 triple1) -> rule3))]
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple4 triple1) -> rule3))]
("Charlie" "is" "young" "-")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Charlie is rough.[(triple5)] Dave is big.[(triple6)] Dave is cold.[(triple7)] Dave is quiet.[(triple8 OR ((triple10 triple6) -> rule2) OR ((((triple7) -> rule1) triple6) -> rule2) OR ((((triple9 triple7) -> rule3) triple6) -> rule2))] Dave is red.[(triple9)] Dave is young.[(triple10 OR ((triple7) -> rule1) OR ((triple9 triple7) -> rule3))] @1: Charlie is young.[(((triple1) -> rule1) OR ((triple4 triple1) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple10 triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple9 triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple7) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple9 triple7) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1