Anne is blue. Anne is not furry. Bob is cold. Bob is furry. Bob is rough. Charlie is white. Harry is rough. All smart, rough people are white. If Bob is green and Bob is rough then Bob is blue. Blue, rough people are smart. All rough, green people are cold. If someone is blue and not furry then they are cold. If Charlie is smart then Charlie is not cold. Cold people are green. If someone is cold and white then they are green. Cold, green people are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All smart, rough people are white.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Bob is green and Bob is rough then Bob is blue.
((("Bob" "is" "green" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "blue" "+"))
Blue, rough people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All rough, green people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and not furry then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "cold" "+"))
If Charlie is smart then Charlie is not cold.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "cold" "-"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and white then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Cold, green people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Bob is furry.
True
1
proof
[(triple4)]
("Bob" "is" "furry" "+")
triple4
Bob is not furry.
False
1
inv-proof
[(triple4)]
("Bob" "is" "furry" "-")
triple4
Bob is green.
True
2
proof
[(((triple3) -> rule7))]
("Bob" "is" "green" "+")
((triple3) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple3) -> rule7))]
("Bob" "is" "green" "-")
((triple3) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is green.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule7))]
("Anne" "is" "green" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not green.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule7))]
("Anne" "is" "green" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
True
8
proof
[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9))]
("Anne" "is" "rough" "+")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not rough.
False
8
inv-proof
[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9))]
("Anne" "is" "rough" "-")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
True
10
proof
[(((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3))]
("Anne" "is" "smart" "+")
((triple1 ((((triple1 triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not smart.
False
10
inv-proof
[(((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3))]
("Anne" "is" "smart" "-")
((triple1 ((((triple1 triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is white.
True
19
proof
[(((((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3) ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule1))]
("Anne" "is" "white" "+")
((((triple1 ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Anne is not white.
False
19
inv-proof
[(((((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3) ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule1))]
("Anne" "is" "white" "-")
((((triple1 ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Harry is not cold.
Unknown
inv-rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not green.
Unknown
inv-rconc
[@4: Charlie is green.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule9 <- rule5 <- FAIL)]]
("Charlie" "is" "green" "-")
Harry is green.
Unknown
rconc
[@4: Harry is green.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is cold.
Unknown
rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- rule9 <- rule5 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is not furry.[(triple2)] Bob is cold.[(triple3)] Bob is furry.[(triple4)] Bob is rough.[(triple5 OR ((triple3 ((triple3) -> rule7)) -> rule9))] Charlie is white.[(triple6)] Harry is rough.[(triple7)] @1: Anne is cold.[(((triple1 triple2) -> rule5))] Bob is green.[(((triple3) -> rule7))] @2: Anne is green.[(((((triple1 triple2) -> rule5)) -> rule7))] Bob is blue.[(((((triple3) -> rule7) triple5) -> rule2) OR ((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2))] @3: Anne is rough.[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9))] Bob is smart.[(((((((triple3) -> rule7) triple5) -> rule2) triple5) -> rule3) OR ((((((triple3) -> rule7) triple5) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3) OR ((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) triple5) -> rule3) OR ((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3))] @4: Anne is smart.[(((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3))] Bob is white.[(((((((((triple3) -> rule7) triple5) -> rule2) triple5) -> rule3) triple5) -> rule1) OR ((((((((triple3) -> rule7) triple5) -> rule2) triple5) -> rule3) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule1) OR ((((((((triple3) -> rule7) triple5) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3) triple5) -> rule1) OR ((((((((triple3) -> rule7) triple5) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule1) OR ((((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) triple5) -> rule3) triple5) -> rule1) OR ((((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) triple5) -> rule3) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule1) OR ((((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3) triple5) -> rule1) OR ((((((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule2) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule3) ((triple3 ((triple3) -> rule7)) -> rule9)) -> rule1))] @5: Anne is white.[(((((triple1 ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule3) ((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule7)) -> rule9)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3 ((triple3) -> (rule7 % int2))) -> (rule9 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple3) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule7 % int2)) triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple3) -> (rule7 % int3)) ((triple3 ((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple3) -> (rule7 % int3)) triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple3) -> (rule7 % int4)) triple5) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule7 % int4))) -> (rule9 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple3) -> (rule7 % int4)) ((triple3 ((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple3) -> (rule7 % int4)) ((triple3 ((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) ((triple3 ((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((((triple1 triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
((((((((triple3) -> (rule7 % int4)) triple5) -> (rule2 % int3)) triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((((triple3) -> (rule7 % int5)) triple5) -> (rule2 % int4)) triple5) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) triple5) -> (rule2 % int4)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) triple5) -> (rule2 % int4)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int3))) -> (rule3 % int2)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule2 % int3)) triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule2 % int3)) triple5) -> (rule3 % int2)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
((((((((triple3) -> (rule7 % int5)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule3 % int2)) ((triple3 ((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Anne is white.
("Anne" "is" "white" "+")
((((triple1 ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule3 % int2)) ((((triple1 triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5