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