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