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