Bob is green. Erin is furry. Erin is green. Erin is quiet. Erin is red. Erin is round. Erin is white. Fiona is furry. Fiona is green. Fiona is round. Gary is red. Gary is white. Quiet things are furry. All smart things are quiet. If something is green then it is white. If something is round then it is smart. All white, green things are round. If Erin is red and Erin is green then Erin is white.
Bob is green.
("Bob" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All white, green things are round.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Erin is red and Erin is green then Erin is white.
((("Erin" "is" "red" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "white" "+"))
Fiona is round.
True
1
proof
[(triple10 OR ((((triple9) -> rule3) triple9) -> rule5))]
("Fiona" "is" "round" "+")
triple10
((((triple9) -> (rule3 % int2)) triple9) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Gary is not red.
False
1
inv-proof
[(triple11)]
("Gary" "is" "red" "-")
triple11
Fiona is white.
True
2
proof
[(((triple9) -> rule3))]
("Fiona" "is" "white" "+")
((triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((((triple9) -> rule3) triple9) -> rule5)) -> rule4))]
("Fiona" "is" "smart" "-")
((triple10) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple9) -> (rule3 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Bob is round.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule5))]
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule5))]
("Bob" "is" "round" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
True
5
proof
[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule4))]
("Bob" "is" "smart" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
False
5
inv-proof
[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule4))]
("Bob" "is" "smart" "-")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
True
6
proof
[(((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "quiet" "+")
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not quiet.
False
6
inv-proof
[(((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "quiet" "-")
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is furry.
True
7
proof
[(((((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2)) -> rule1))]
("Bob" "is" "furry" "+")
((((((((((triple1) -> (rule3 % int5)) triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not furry.
False
7
inv-proof
[(((((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2)) -> rule1))]
("Bob" "is" "furry" "-")
((((((((((triple1) -> (rule3 % int5)) triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is quiet.
Unknown
rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is furry.
Unknown
rconc
[@4: Gary is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is green.[(triple1)] Erin is furry.[(triple2 OR ((triple4) -> rule1) OR ((((((triple6) -> rule4)) -> rule2)) -> rule1) OR ((((((((triple7 triple3) -> rule5)) -> rule4)) -> rule2)) -> rule1) OR ((((((((((triple3) -> rule3) triple3) -> rule5)) -> rule4)) -> rule2)) -> rule1) OR ((((((((((triple5 triple3) -> rule6) triple3) -> rule5)) -> rule4)) -> rule2)) -> rule1))] Erin is green.[(triple3)] Erin is quiet.[(triple4 OR ((((triple6) -> rule4)) -> rule2) OR ((((((triple7 triple3) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple3) -> rule3) triple3) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple5 triple3) -> rule6) triple3) -> rule5)) -> rule4)) -> rule2))] Erin is red.[(triple5)] Erin is round.[(triple6 OR ((triple7 triple3) -> rule5) OR ((((triple3) -> rule3) triple3) -> rule5) OR ((((triple5 triple3) -> rule6) triple3) -> rule5))] Erin is white.[(triple7 OR ((triple3) -> rule3) OR ((triple5 triple3) -> rule6))] Fiona is furry.[(triple8 OR ((((((triple10) -> rule4)) -> rule2)) -> rule1) OR ((((((((((triple9) -> rule3) triple9) -> rule5)) -> rule4)) -> rule2)) -> rule1))] Fiona is green.[(triple9)] Fiona is round.[(triple10 OR ((((triple9) -> rule3) triple9) -> rule5))] Gary is red.[(triple11)] Gary is white.[(triple12)] @1: Bob is white.[(((triple1) -> rule3))] Erin is smart.[(((triple6) -> rule4) OR ((((triple7 triple3) -> rule5)) -> rule4) OR ((((((triple3) -> rule3) triple3) -> rule5)) -> rule4) OR ((((((triple5 triple3) -> rule6) triple3) -> rule5)) -> rule4))] Fiona is smart.[(((triple10) -> rule4) OR ((((((triple9) -> rule3) triple9) -> rule5)) -> rule4))] Fiona is white.[(((triple9) -> rule3))] @2: Bob is round.[(((((triple1) -> rule3) triple1) -> rule5))] Fiona is quiet.[(((((triple10) -> rule4)) -> rule2) OR ((((((((triple9) -> rule3) triple9) -> rule5)) -> rule4)) -> rule2))] @3: Bob is smart.[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule4))] @4: Bob is quiet.[(((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2))] @5: Bob is furry.[(((((((((((triple1) -> rule3) triple1) -> rule5)) -> rule4)) -> rule2)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple4) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((((triple7 triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((((((triple3) -> (rule3 % int5)) triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
((((((((((triple5 triple3) -> (rule6 % int5)) triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple7 triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple5 triple3) -> (rule6 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple7 triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple3) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5 triple3) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5 triple3) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((((triple9) -> (rule3 % int5)) triple9) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
int5
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((((triple9) -> (rule3 % int2)) triple9) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple3) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5 triple3) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple10) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((((triple9) -> (rule3 % int3)) triple9) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((((triple9) -> (rule3 % int4)) triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
((((((((((triple1) -> (rule3 % int5)) triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5