Anne is not cold. Anne is rough. Anne is smart. Dave is big. Dave is cold. Dave is green. Dave is rough. Dave is round. Gary is big. Gary is not cold. Gary is green. Gary is rough. Gary is smart. Gary is white. Harry is cold. Harry is white. Round things are white. If something is round and white then it is cold.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is white.
("Harry" "is" "white" "+")
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is round and white then it is cold.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Gary is not green.
False
1
inv-proof
[(triple11)]
("Gary" "is" "green" "-")
triple11
Dave is white.
True
2
proof
[(((triple8) -> rule1))]
("Dave" "is" "white" "+")
((triple8) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple8) -> rule1))]
("Dave" "is" "white" "-")
((triple8) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is not cold.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3)] Dave is big.[(triple4)] Dave is cold.[(triple5 OR ((triple8 ((triple8) -> rule1)) -> rule2))] Dave is green.[(triple6)] Dave is rough.[(triple7)] Dave is round.[(triple8)] Gary is big.[(triple9)] Gary is green.[(triple11)] Gary is not cold.[(triple10)] Gary is rough.[(triple12)] Gary is smart.[(triple13)] Gary is white.[(triple14)] Harry is cold.[(triple15)] Harry is white.[(triple16)] @1: Dave is white.[(((triple8) -> rule1))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
Harry is cold.
("Harry" "is" "cold" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Dave is white.
("Dave" "is" "white" "+")
((triple8) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1