Charlie is smart. Gary is rough. Harry is big. All cold, big things are red. If Harry is round then Harry is big. If Harry is big and Harry is smart then Harry is rough. If something is cold then it is round. If Harry is nice and Harry is smart then Harry is cold. If something is rough then it is cold. If Gary is red and Gary is cold then Gary is smart. If Charlie is nice and Charlie is rough then Charlie is red.
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
All cold, big things are red.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Harry is round then Harry is big.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
If Harry is big and Harry is smart then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Harry is nice and Harry is smart then Harry is cold.
((("Harry" "is" "nice" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "cold" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Gary is red and Gary is cold then Gary is smart.
((("Gary" "is" "red" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
If Charlie is nice and Charlie is rough then Charlie is red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "red" "+"))
Harry is big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Gary is cold.
True
2
proof
[(((triple2) -> rule6))]
("Gary" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("Gary" "is" "cold" "-")
((triple2) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is red.
Unknown
rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("Harry" "is" "red" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is smart.[(triple1)] Gary is rough.[(triple2)] Harry is big.[(triple3)] @1: Gary is cold.[(((triple2) -> rule6))] @2: Gary is round.[(((((triple2) -> rule6)) -> rule4))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2