Anne is big. Anne is green. Anne is red. Anne is rough. Bob is quiet. Erin is not big. Erin is not cold. Erin is furry. Erin is green. Erin is quiet. Gary is big. Gary is rough. If something is quiet then it is green. If something is furry then it is green. If something is cold then it is red. Cold, green things are red. If something is big then it is red. If Bob is rough then Bob is big. All big, red things are furry. All green, quiet things are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Cold, green things are red.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Bob is rough then Bob is big.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "big" "+"))
All big, red things are furry.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All green, quiet things are rough.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Anne is red.
True
1
proof
[(triple3 OR ((triple1) -> rule5))]
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not quiet.
False
1
inv-proof
[(triple5)]
("Bob" "is" "quiet" "-")
triple5
Gary is red.
True
2
proof
[(((triple11) -> rule5))]
("Gary" "is" "red" "+")
((triple11) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "green" "-")
((triple5) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
True
4
proof
[(((((triple5) -> rule1) triple5) -> rule8))]
("Bob" "is" "rough" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((triple11 ((triple11) -> rule5)) -> rule7))]
("Gary" "is" "furry" "-")
((triple11 ((triple11) -> (rule5 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Bob is big.
True
5
proof
[(((((((triple5) -> rule1) triple5) -> rule8)) -> rule6))]
("Bob" "is" "big" "+")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not big.
False
5
inv-proof
[(((((((triple5) -> rule1) triple5) -> rule8)) -> rule6))]
("Bob" "is" "big" "-")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
True
6
proof
[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5))]
("Bob" "is" "red" "+")
((((((((triple5) -> (rule1 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not red.
False
6
inv-proof
[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5))]
("Bob" "is" "red" "-")
((((((((triple5) -> (rule1 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is furry.
True
12
proof
[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6) ((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5)) -> rule7))]
("Bob" "is" "furry" "+")
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Bob is not furry.
False
12
inv-proof
[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6) ((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5)) -> rule7))]
("Bob" "is" "furry" "-")
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
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" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((((triple1 triple3) -> rule7)) -> rule2) OR ((((triple1 ((triple1) -> rule5)) -> rule7)) -> rule2))] Anne is red.[(triple3 OR ((triple1) -> rule5))] Anne is rough.[(triple4)] Bob is quiet.[(triple5)] Erin is furry.[(triple8)] Erin is green.[(triple9 OR ((triple10) -> rule1) OR ((triple8) -> rule2))] Erin is not big.[(triple6)] Erin is not cold.[(triple7)] Erin is quiet.[(triple10)] Gary is big.[(triple11)] Gary is rough.[(triple12)] @1: Anne is furry.[(((triple1 triple3) -> rule7) OR ((triple1 ((triple1) -> rule5)) -> rule7))] Bob is green.[(((triple5) -> rule1))] Erin is rough.[(((triple9 triple10) -> rule8) OR ((((triple10) -> rule1) triple10) -> rule8) OR ((((triple8) -> rule2) triple10) -> rule8))] Gary is red.[(((triple11) -> rule5))] @2: Bob is rough.[(((((triple5) -> rule1) triple5) -> rule8))] Gary is furry.[(((triple11 ((triple11) -> rule5)) -> rule7))] @3: Bob is big.[(((((((triple5) -> rule1) triple5) -> rule8)) -> rule6))] Gary is green.[(((((triple11 ((triple11) -> rule5)) -> rule7)) -> rule2))] @4: Bob is red.[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5))] @5: Bob is furry.[(((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6) ((((((((triple5) -> rule1) triple5) -> rule8)) -> rule6)) -> rule5)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((((triple1 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
((triple10) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
triple6
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple3) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple5) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple9 triple10) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple10) -> (rule1 % int2)) triple10) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8) -> (rule2 % int2)) triple10) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple11) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple11 ((triple11) -> (rule5 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple11 ((triple11) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((((((triple5) -> (rule1 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5