Charlie is cold. Charlie is green. Charlie is quiet. Charlie is smart. Dave is round. Dave is smart. Dave is young. All green things are white. Smart things are round. If Dave is young then Dave is green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Dave is young then Dave is green.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "green" "+"))
Dave is young.
True
1
proof
[(triple7)]
("Dave" "is" "young" "+")
triple7
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Dave is green.
True
2
proof
[(((triple7) -> rule3))]
("Dave" "is" "green" "+")
((triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple7) -> rule3))]
("Dave" "is" "green" "-")
((triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("Dave" "is" "white" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("Dave" "is" "white" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Charlie is quiet.[(triple3)] Charlie is smart.[(triple4)] Dave is round.[(triple5 OR ((triple6) -> rule2))] Dave is smart.[(triple6)] Dave is young.[(triple7)] @1: Charlie is round.[(((triple4) -> rule2))] Charlie is white.[(((triple2) -> rule1))] Dave is green.[(((triple7) -> rule3))] @2: Dave is white.[(((((triple7) -> rule3)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2