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