Bob is nice. Gary is big. Furry things are big. If Bob is kind then Bob is big. If something is big then it is nice. If something is kind and rough then it is cold. If something is big and nice then it is furry. All big things are quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Bob is kind then Bob is big.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "big" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is kind and rough then it is cold.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is big and nice then it is furry.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Gary is big.
True
1
proof
[(triple2)]
("Gary" "is" "big" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple2)]
("Gary" "is" "big" "-")
triple2
Gary is nice.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Gary" "is" "furry" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Gary" "is" "furry" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Gary is big.[(triple2)] @1: Gary is nice.[(((triple2) -> rule3))] Gary is quiet.[(((triple2) -> rule6))] @2: Gary is furry.[(((triple2 ((triple2) -> rule3)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2