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