Anne is not cold. Bob is round. Dave is big. Dave is not furry. Dave is round. Gary is not red. Gary is round. Furry things are white. If something is smart and round then it is white. If Bob is round then Bob is smart. If something is furry then it is cold. White, smart things are furry. All furry things are smart. All big things are red. Cold things are not red.
Anne is not cold.
("Anne" "is" "cold" "-")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is round.
("Dave" "is" "round" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is round.
("Gary" "is" "round" "+")
Furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is smart and round then it is white.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Bob is round then Bob is smart.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "smart" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
White, smart things are furry.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Cold things are not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
Gary is not red.
True
1
proof
[(triple6)]
("Gary" "is" "red" "-")
triple6
Dave is not big.
False
1
inv-proof
[(triple3)]
("Dave" "is" "big" "-")
triple3
Bob is smart.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "red" "-")
((triple3) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is white.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not white.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Bob" "is" "white" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
True
7
proof
[(((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not furry.
False
7
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "furry" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is cold.
True
8
proof
[(((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4))]
("Bob" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3)) ((triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not cold.
False
8
inv-proof
[(((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4))]
("Bob" "is" "cold" "-")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3)) ((triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not red.
True
9
proof
[(((((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4)) -> rule8))]
("Bob" "is" "red" "-")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule2 % int4)) ((triple2) -> (rule3 % int5))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is red.
False
9
inv-proof
[(((((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4)) -> rule8))]
("Bob" "is" "red" "+")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule2 % int4)) ((triple2) -> (rule3 % int5))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is white.
Unknown
rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "cold" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is not cold.[(triple1)] Bob is round.[(triple2)] Dave is big.[(triple3)] Dave is not furry.[(triple4)] Dave is round.[(triple5)] Gary is not red.[(triple6)] Gary is round.[(triple7)] @1: Bob is smart.[(((triple2) -> rule3))] Dave is red.[(((triple3) -> rule7))] @2: Bob is white.[(((((triple2) -> rule3) triple2) -> rule2))] @3: Bob is furry.[(((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5))] @4: Bob is cold.[(((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4))] @5: Bob is not red.[(((((((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule5)) -> rule4)) -> rule8))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is not red.
("Gary" "is" "red" "-")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3)) ((triple2) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not red.
("Bob" "is" "red" "-")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule2 % int4)) ((triple2) -> (rule3 % int5))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5