Bob is quiet. Bob is smart. Charlie is cold. Gary is cold. Gary is furry. Gary is green. Gary is quiet. All smart people are quiet. Blue people are cold. All smart people are blue. Smart people are green. If Gary is blue then Gary is furry. If Charlie is green and Charlie is quiet then Charlie is smart.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Gary is blue then Gary is furry.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "furry" "+"))
If Charlie is green and Charlie is quiet then Charlie is smart.
((("Charlie" "is" "green" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "smart" "+"))
Charlie is cold.
True
1
proof
[(triple3)]
("Charlie" "is" "cold" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is green.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "green" "+")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "green" "-")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is quiet.[(triple1 OR ((triple2) -> rule1))] Bob is smart.[(triple2)] Charlie is cold.[(triple3)] Gary is cold.[(triple4)] Gary is furry.[(triple5)] Gary is green.[(triple6)] Gary is quiet.[(triple7)] @1: Bob is blue.[(((triple2) -> rule3))] Bob is green.[(((triple2) -> rule4))] @2: Bob is cold.[(((((triple2) -> rule3)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2