Anne is young. Dave is big. Gary is big. Gary is cold. Gary is rough. Harry is cold. Harry is furry. If something is big then it is round. All big things are cold. Young things are rough.
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Harry is cold.
True
1
proof
[(triple6)]
("Harry" "is" "cold" "+")
triple6
Gary is not cold.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule2))]
("Gary" "is" "cold" "-")
triple4
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is young.[(triple1)] Dave is big.[(triple2)] Gary is big.[(triple3)] Gary is cold.[(triple4 OR ((triple3) -> rule2))] Gary is rough.[(triple5)] Harry is cold.[(triple6)] Harry is furry.[(triple7)] @1: Anne is rough.[(((triple1) -> rule3))] Dave is cold.[(((triple2) -> rule2))] Dave is round.[(((triple2) -> rule1))] Gary is round.[(((triple3) -> rule1))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1