Anne is round. Bob is blue. Bob is green. Bob is quiet. Charlie is blue. Charlie is rough. Fiona is red. All green things are red. If something is smart and quiet then it is green. If Anne is green then Anne is round. Rough, smart things are blue. Green things are red. Red, green things are round. Green things are rough. If something is rough and smart then it is quiet. All blue, rough things are smart.
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is smart and quiet then it is green.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Anne is green then Anne is round.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "round" "+"))
Rough, smart things are blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Red, green things are round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is rough and smart then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All blue, rough things are smart.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple5)]
("Charlie" "is" "blue" "+")
triple5
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Bob is rough.
True
2
proof
[(((triple3) -> rule7))]
("Bob" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is not smart.
False
3
inv-proof
[(((triple5 triple6) -> rule9))]
("Charlie" "is" "smart" "-")
((triple5 triple6) -> (rule9 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is smart.
True
4
proof
[(((triple2 ((triple3) -> rule7)) -> rule9))]
("Bob" "is" "smart" "+")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule9 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule6) OR ((((triple3) -> rule5) triple3) -> rule6))]
("Bob" "is" "round" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is green.
True
9
proof
[(((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2))]
("Charlie" "is" "green" "+")
((((triple5 triple6) -> (rule9 % int3)) ((triple6 ((triple5 triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not green.
False
9
inv-proof
[(((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2))]
("Charlie" "is" "green" "-")
((((triple5 triple6) -> (rule9 % int3)) ((triple6 ((triple5 triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is red.
True
10
proof
[(((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) OR ((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5))]
("Charlie" "is" "red" "+")
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is not red.
False
10
inv-proof
[(((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) OR ((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5))]
("Charlie" "is" "red" "-")
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is round.
True
20
proof
[(((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6))]
("Charlie" "is" "round" "+")
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
Charlie is not round.
False
20
inv-proof
[(((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6))]
("Charlie" "is" "round" "-")
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule9 <- FAIL)]]
("Fiona" "is" "rough" "-")
Anne is green.
Unknown
rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule2 <- rule9 <- rule4 <- FAIL)]]
("Anne" "is" "green" "+")
Fiona is not round.
Unknown
inv-rconc
[@4: Fiona is round.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule9 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is quiet.
Unknown
rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not green.
Unknown
inv-rconc
[@3: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule9 <- rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is round.[(triple1)] Bob is blue.[(triple2)] Bob is green.[(triple3)] Bob is quiet.[(triple4 OR ((((triple3) -> rule7) ((triple2 ((triple3) -> rule7)) -> rule9)) -> rule8))] Charlie is blue.[(triple5)] Charlie is rough.[(triple6)] Fiona is red.[(triple7)] @1: Bob is red.[(((triple3) -> rule1) OR ((triple3) -> rule5))] Bob is rough.[(((triple3) -> rule7))] Charlie is smart.[(((triple5 triple6) -> rule9))] @2: Bob is round.[(((((triple3) -> rule1) triple3) -> rule6) OR ((((triple3) -> rule5) triple3) -> rule6))] Bob is smart.[(((triple2 ((triple3) -> rule7)) -> rule9))] Charlie is quiet.[(((triple6 ((triple5 triple6) -> rule9)) -> rule8))] @3: Charlie is green.[(((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2))] @4: Charlie is red.[(((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) OR ((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5))] @5: Charlie is round.[(((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule1) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6) OR ((((((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule5) ((((triple5 triple6) -> rule9) ((triple6 ((triple5 triple6) -> rule9)) -> rule8)) -> rule2)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((((triple3) -> (rule7 % int3)) ((triple2 ((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5 triple6) -> (rule9 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule9 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6 ((triple5 triple6) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple5 triple6) -> (rule9 % int3)) ((triple6 ((triple5 triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((triple5 triple6) -> (rule9 % int4)) ((triple6 ((triple5 triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
((((((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple5 triple6) -> (rule9 % int5)) ((triple6 ((triple5 triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5