Anne is furry. Anne is red. Erin is smart. Gary is kind. Gary is red. Gary is rough. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is rough. Harry is smart. Green, kind people are blue. Green people are smart. All rough people are green. If someone is rough and furry then they are blue. All rough, kind people are green. Red people are rough.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green, kind people are blue.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and furry then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All rough, kind people are green.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Gary is not red.
False
1
inv-proof
[(triple5)]
("Gary" "is" "red" "-")
triple5
Gary is green.
True
2
proof
[(((triple6) -> rule3) OR ((triple6 triple4) -> rule5) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6) triple4) -> rule5))]
("Gary" "is" "green" "+")
((triple6) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple6 triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple5) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "rough" "-")
((triple2) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
True
4
proof
[(((((triple2) -> rule6) triple1) -> rule4))]
("Anne" "is" "blue" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Anne" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule2))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule2))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Erin is smart.[(triple3)] Gary is kind.[(triple4)] Gary is red.[(triple5)] Gary is rough.[(triple6 OR ((triple5) -> rule6))] Harry is furry.[(triple7)] Harry is green.[(triple8 OR ((triple11) -> rule3) OR ((triple11 triple9) -> rule5) OR ((((triple10) -> rule6)) -> rule3) OR ((((triple10) -> rule6) triple9) -> rule5))] Harry is kind.[(triple9)] Harry is red.[(triple10)] Harry is rough.[(triple11 OR ((triple10) -> rule6))] Harry is smart.[(triple12 OR ((triple8) -> rule2) OR ((((triple11) -> rule3)) -> rule2) OR ((((triple11 triple9) -> rule5)) -> rule2) OR ((((((triple10) -> rule6)) -> rule3)) -> rule2) OR ((((((triple10) -> rule6) triple9) -> rule5)) -> rule2))] @1: Anne is rough.[(((triple2) -> rule6))] Gary is green.[(((triple6) -> rule3) OR ((triple6 triple4) -> rule5) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6) triple4) -> rule5))] Harry is blue.[(((triple11 triple7) -> rule4) OR ((triple8 triple9) -> rule1) OR ((((triple10) -> rule6) triple7) -> rule4) OR ((((triple11) -> rule3) triple9) -> rule1) OR ((((triple11 triple9) -> rule5) triple9) -> rule1) OR ((((((triple10) -> rule6)) -> rule3) triple9) -> rule1) OR ((((((triple10) -> rule6) triple9) -> rule5) triple9) -> rule1))] @2: Anne is blue.[(((((triple2) -> rule6) triple1) -> rule4))] Anne is green.[(((((triple2) -> rule6)) -> rule3))] Gary is blue.[(((((triple6) -> rule3) triple4) -> rule1) OR ((((triple6 triple4) -> rule5) triple4) -> rule1) OR ((((((triple5) -> rule6)) -> rule3) triple4) -> rule1) OR ((((((triple5) -> rule6) triple4) -> rule5) triple4) -> rule1))] Gary is smart.[(((((triple6) -> rule3)) -> rule2) OR ((((triple6 triple4) -> rule5)) -> rule2) OR ((((((triple5) -> rule6)) -> rule3)) -> rule2) OR ((((((triple5) -> rule6) triple4) -> rule5)) -> rule2))] @3: Anne is smart.[(((((((triple2) -> rule6)) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple11 triple9) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple10) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple10) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple8) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple10) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple6 triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple5) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple11 triple7) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple8 triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2)) triple7) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple11) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11 triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple10) -> (rule6 % int3)) triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6 triple4) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple5) -> (rule6 % int3)) triple4) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple5) -> (rule6 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3