Anne is cold. Anne is green. Anne is kind. Anne is quiet. Anne is rough. Anne is smart. Anne is white. Bob is kind. Bob is white. Erin is green. Erin is quiet. Harry is cold. If something is white and rough then it is kind. Kind things are smart. Kind, quiet things are cold. If Harry is quiet then Harry is white. Cold things are quiet. All smart, quiet things are green. Green things are smart. White things are kind. If something is green and rough then it is smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If something is white and rough then it is kind.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Kind, quiet things are cold.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Harry is quiet then Harry is white.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "white" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All smart, quiet things are green.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is green and rough then it is smart.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Anne is green.
True
1
proof
[(triple2 OR ((triple6 triple4) -> rule6) OR ((triple6 ((triple1) -> rule5)) -> rule6) OR ((((triple3) -> rule2) triple4) -> rule6) OR ((((triple3) -> rule2) ((triple1) -> rule5)) -> rule6) OR ((((((triple7) -> rule8)) -> rule2) triple4) -> rule6) OR ((((((triple7 triple5) -> rule1)) -> rule2) triple4) -> rule6) OR ((((((triple7) -> rule8)) -> rule2) ((triple1) -> rule5)) -> rule6) OR ((((((triple7 triple5) -> rule1)) -> rule2) ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "green" "+")
triple2
((triple6 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple6 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple3) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple7 triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple7) -> (rule8 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((triple7 triple5) -> (rule1 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Erin is not green.
False
1
inv-proof
[(triple10)]
("Erin" "is" "green" "-")
triple10
Bob is smart.
True
2
proof
[(((triple8) -> rule2) OR ((((triple9) -> rule8)) -> rule2))]
("Bob" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple10) -> rule7))]
("Erin" "is" "smart" "-")
((triple10) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is white.
True
3
proof
[(((((triple12) -> rule5)) -> rule4))]
("Harry" "is" "white" "+")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule4))]
("Harry" "is" "white" "-")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
True
4
proof
[(((((((triple12) -> rule5)) -> rule4)) -> rule8))]
("Harry" "is" "kind" "+")
((((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not kind.
False
4
inv-proof
[(((((((triple12) -> rule5)) -> rule4)) -> rule8))]
("Harry" "is" "kind" "-")
((((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
True
5
proof
[(((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2))]
("Harry" "is" "smart" "+")
((((((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not smart.
False
5
inv-proof
[(((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2))]
("Harry" "is" "smart" "-")
((((((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is green.
True
8
proof
[(((((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2) ((triple12) -> rule5)) -> rule6))]
("Harry" "is" "green" "+")
((((((((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((triple12) -> (rule5 % int5))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is not green.
False
8
inv-proof
[(((((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2) ((triple12) -> rule5)) -> rule6))]
("Harry" "is" "green" "-")
((((((((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((triple12) -> (rule5 % int5))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is cold.[(triple1 OR ((triple3 triple4) -> rule3) OR ((((triple7) -> rule8) triple4) -> rule3) OR ((((triple7 triple5) -> rule1) triple4) -> rule3))] Anne is green.[(triple2 OR ((triple6 triple4) -> rule6) OR ((triple6 ((triple1) -> rule5)) -> rule6) OR ((((triple3) -> rule2) triple4) -> rule6) OR ((((triple3) -> rule2) ((triple1) -> rule5)) -> rule6) OR ((((((triple7) -> rule8)) -> rule2) triple4) -> rule6) OR ((((((triple7 triple5) -> rule1)) -> rule2) triple4) -> rule6) OR ((((((triple7) -> rule8)) -> rule2) ((triple1) -> rule5)) -> rule6) OR ((((((triple7 triple5) -> rule1)) -> rule2) ((triple1) -> rule5)) -> rule6))] Anne is kind.[(triple3 OR ((triple7) -> rule8) OR ((triple7 triple5) -> rule1))] Anne is quiet.[(triple4 OR ((triple1) -> rule5))] Anne is rough.[(triple5)] Anne is smart.[(triple6 OR ((triple2) -> rule7) OR ((triple3) -> rule2) OR ((triple2 triple5) -> rule9) OR ((((triple7) -> rule8)) -> rule2) OR ((((triple7 triple5) -> rule1)) -> rule2))] Anne is white.[(triple7)] Bob is kind.[(triple8 OR ((triple9) -> rule8))] Bob is white.[(triple9)] Erin is green.[(triple10)] Erin is quiet.[(triple11)] Harry is cold.[(triple12)] @1: Bob is smart.[(((triple8) -> rule2) OR ((((triple9) -> rule8)) -> rule2))] Erin is smart.[(((triple10) -> rule7))] Harry is quiet.[(((triple12) -> rule5))] @2: Harry is white.[(((((triple12) -> rule5)) -> rule4))] @3: Harry is kind.[(((((((triple12) -> rule5)) -> rule4)) -> rule8))] @4: Harry is smart.[(((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2))] @5: Harry is green.[(((((((((((triple12) -> rule5)) -> rule4)) -> rule8)) -> rule2) ((triple12) -> rule5)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple3 triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple7) -> (rule8 % int2)) triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple7 triple5) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple6 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple6 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple3) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple7 triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple7) -> (rule8 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((triple7 triple5) -> (rule1 % int4))) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple7) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple7 triple5) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 triple5) -> (rule9 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple7 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
triple8
((triple9) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple10) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple12) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((((triple12) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((((((((((triple12) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((triple12) -> (rule5 % int5))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5