Bob is green. Charlie is big. Dave is quiet. Gary is furry. All round, cold things are quiet. If something is cold then it is round. If something is furry then it is cold.
Bob is green.
("Bob" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All round, cold things are quiet.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Gary is cold.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "cold" "-")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "round" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "round" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
True
6
proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule1))]
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not quiet.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule1))]
("Gary" "is" "quiet" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "round" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is green.[(triple1)] Charlie is big.[(triple2)] Dave is quiet.[(triple3)] Gary is furry.[(triple4)] @1: Gary is cold.[(((triple4) -> rule3))] @2: Gary is round.[(((((triple4) -> rule3)) -> rule2))] @3: Gary is quiet.[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3