Anne is kind. Anne is young. Bob is furry. Bob is not red. Gary is kind. Gary is not red. Gary is round. Round, big things are not cold. All kind things are big. If something is big and not round then it is furry. If something is big and not round then it is furry. Furry things are kind. If something is big and furry then it is not red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not red.
("Bob" "is" "red" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is round.
("Gary" "is" "round" "+")
Round, big things are not cold.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "-"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is big and not round then it is furry.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "furry" "+"))
If something is big and not round then it is furry.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "furry" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is big and furry then it is not red.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "-"))
Bob is not red.
True
1
proof
[(triple4 OR ((((((triple3) -> rule5)) -> rule2) triple3) -> rule6))]
("Bob" "is" "red" "-")
triple4
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is not cold.
True
4
proof
[(((triple7 ((triple5) -> rule2)) -> rule1))]
("Gary" "is" "cold" "-")
((triple7 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("Bob" "is" "big" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is kind.[(triple1)] Anne is young.[(triple2)] Bob is furry.[(triple3)] Bob is not red.[(triple4 OR ((((((triple3) -> rule5)) -> rule2) triple3) -> rule6))] Gary is kind.[(triple5)] Gary is not red.[(triple6)] Gary is round.[(triple7)] @1: Anne is big.[(((triple1) -> rule2))] Bob is kind.[(((triple3) -> rule5))] Gary is big.[(((triple5) -> rule2))] @2: Bob is big.[(((((triple3) -> rule5)) -> rule2))] Gary is not cold.[(((triple7 ((triple5) -> rule2)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is not red.
("Bob" "is" "red" "-")
triple4
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is not red.
("Gary" "is" "red" "-")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((triple7 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2