Anne is blue. Anne is furry. Anne is round. Bob is cold. Bob is young. Erin is blue. Erin is cold. Erin is furry. Erin is rough. Erin is round. Gary is green. Gary is round. If someone is blue and round then they are rough. If someone is green and rough then they are furry. Young people are green. All blue, cold people are rough. Furry, green people are blue. Cold, green people are blue. If someone is furry and young then they are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is blue and round then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and rough then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All blue, cold people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Furry, green people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Cold, green people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry and young then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Bob is cold.
True
1
proof
[(triple4)]
("Bob" "is" "cold" "+")
triple4
Erin is not blue.
False
1
inv-proof
[(triple6)]
("Erin" "is" "blue" "-")
triple6
Anne is rough.
True
3
proof
[(((triple1 triple3) -> rule1))]
("Anne" "is" "rough" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
3
inv-proof
[(((triple1 triple3) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is blue.
True
4
proof
[(((triple4 ((triple5) -> rule3)) -> rule6))]
("Bob" "is" "blue" "+")
((triple4 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple4 ((triple5) -> rule3)) -> rule6))]
("Bob" "is" "blue" "-")
((triple4 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
True
6
proof
[(((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4))]
("Bob" "is" "rough" "+")
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not rough.
False
6
inv-proof
[(((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4))]
("Bob" "is" "rough" "-")
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is furry.
True
9
proof
[(((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2))]
("Bob" "is" "furry" "+")
((((triple5) -> (rule3 % int4)) ((((triple4 ((triple5) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not furry.
False
9
inv-proof
[(((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2))]
("Bob" "is" "furry" "-")
((((triple5) -> (rule3 % int4)) ((((triple4 ((triple5) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is round.
True
11
proof
[(((((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2) triple5) -> rule7))]
("Bob" "is" "round" "+")
((((((triple5) -> (rule3 % int5)) ((((triple4 ((triple5) -> (rule3 % int5))) -> (rule6 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Bob is not round.
False
11
inv-proof
[(((((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2) triple5) -> rule7))]
("Bob" "is" "round" "-")
((((((triple5) -> (rule3 % int5)) ((((triple4 ((triple5) -> (rule3 % int5))) -> (rule6 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "+")
Gary is not blue.
Unknown
inv-rconc
[@4: Gary is blue.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is rough.
Unknown
rconc
[@4: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not furry.
Unknown
inv-rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Gary" "is" "furry" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is round.[(triple3)] Bob is cold.[(triple4)] Bob is young.[(triple5)] Erin is blue.[(triple6)] Erin is cold.[(triple7)] Erin is furry.[(triple8)] Erin is rough.[(triple9 OR ((triple6 triple10) -> rule1) OR ((triple6 triple7) -> rule4))] Erin is round.[(triple10)] Gary is green.[(triple11)] Gary is round.[(triple12)] @1: Anne is rough.[(((triple1 triple3) -> rule1))] Bob is green.[(((triple5) -> rule3))] @2: Bob is blue.[(((triple4 ((triple5) -> rule3)) -> rule6))] @3: Bob is rough.[(((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4))] @4: Bob is furry.[(((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2))] @5: Bob is round.[(((((((triple5) -> rule3) ((((triple4 ((triple5) -> rule3)) -> rule6) triple4) -> rule4)) -> rule2) triple5) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple6 triple10) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple6 triple7) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple5) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple4 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((triple5) -> (rule3 % int4)) ((((triple4 ((triple5) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((((((triple5) -> (rule3 % int5)) ((((triple4 ((triple5) -> (rule3 % int5))) -> (rule6 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5