Bob is red. Charlie is cold. Charlie is round. Dave is cold. Dave is kind. Gary is cold. Gary is kind. All smart people are cold. Quiet, red people are cold. Cold people are smart. All blue people are round. If someone is round and cold then they are red. If Dave is cold then Dave is blue. Round, cold people are quiet. Quiet, cold people are kind.
Bob is red.
("Bob" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Quiet, red people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is round and cold then they are red.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Dave is cold then Dave is blue.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "blue" "+"))
Round, cold people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, cold people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Gary is kind.
True
1
proof
[(triple7)]
("Gary" "is" "kind" "+")
triple7
Dave is not cold.
False
1
inv-proof
[(triple4)]
("Dave" "is" "cold" "-")
triple4
Dave is blue.
True
2
proof
[(((triple4) -> rule6))]
("Dave" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple4) -> rule6))]
("Dave" "is" "blue" "-")
((triple4) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Charlie is kind.
True
5
proof
[(((((triple3 triple2) -> rule7) triple2) -> rule8))]
("Charlie" "is" "kind" "+")
((((triple3 triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not kind.
False
5
inv-proof
[(((((triple3 triple2) -> rule7) triple2) -> rule8))]
("Charlie" "is" "kind" "-")
((((triple3 triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is quiet.
True
5
proof
[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule7))]
("Dave" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not red.
False
5
inv-proof
[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule5))]
("Dave" "is" "red" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "+")
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- rule7 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is kind.
Unknown
rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is red.[(triple1)] Charlie is cold.[(triple2)] Charlie is round.[(triple3)] Dave is cold.[(triple4)] Dave is kind.[(triple5 OR ((((((((triple4) -> rule6)) -> rule4) triple4) -> rule7) triple4) -> rule8))] Gary is cold.[(triple6)] Gary is kind.[(triple7)] @1: Charlie is quiet.[(((triple3 triple2) -> rule7))] Charlie is red.[(((triple3 triple2) -> rule5))] Charlie is smart.[(((triple2) -> rule3))] Dave is blue.[(((triple4) -> rule6))] Dave is smart.[(((triple4) -> rule3))] Gary is smart.[(((triple6) -> rule3))] @2: Charlie is kind.[(((((triple3 triple2) -> rule7) triple2) -> rule8))] Dave is round.[(((((triple4) -> rule6)) -> rule4))] @3: Dave is quiet.[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule7))] Dave is red.[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((((((((triple4) -> (rule6 % int4))) -> (rule4 % int3)) triple4) -> (rule7 % int2)) triple4) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3 triple2) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple3 triple2) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple3 triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3