Anne is furry. Anne is nice. Anne is young. Bob is furry. Dave is big. Dave is nice. Dave is white. Gary is red. Gary is white. Gary is young. Cold people are white. If someone is white then they are nice. Nice people are big. If Bob is red then Bob is nice. All nice people are red. All big, red people are cold.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Bob is red then Bob is nice.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "nice" "+"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All big, red people are cold.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Gary is red.
True
1
proof
[(triple8 OR ((((triple9) -> rule2)) -> rule5))]
("Gary" "is" "red" "+")
triple8
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is not big.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule3) OR ((((triple7) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
triple5
((triple6) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Anne is red.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "red" "+")
((triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "big" "-")
((triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
True
5
proof
[(((((triple2) -> rule3) ((triple2) -> rule5)) -> rule6))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule3 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Gary is not big.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule3))]
("Gary" "is" "big" "-")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is white.
True
6
proof
[(((((((triple2) -> rule3) ((triple2) -> rule5)) -> rule6)) -> rule1))]
("Anne" "is" "white" "+")
((((((triple2) -> (rule3 % int4)) ((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Gary is not cold.
False
5
inv-proof
[(((((((triple9) -> rule2)) -> rule3) triple8) -> rule6) OR ((((((triple9) -> rule2)) -> rule3) ((((triple9) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "cold" "-")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple9) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Bob is not white.
Unknown
inv-rconc
[@4: Bob is white.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is nice.
Unknown
rconc
[@5: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule6 <- rule5 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is red.
Unknown
rconc
[@4: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is nice.[(triple2)] Anne is young.[(triple3)] Bob is furry.[(triple4)] Dave is big.[(triple5 OR ((triple6) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] Dave is nice.[(triple6 OR ((triple7) -> rule2))] Dave is white.[(triple7 OR ((((triple5 ((triple6) -> rule5)) -> rule6)) -> rule1) OR ((((((triple6) -> rule3) ((triple6) -> rule5)) -> rule6)) -> rule1))] Gary is red.[(triple8 OR ((((triple9) -> rule2)) -> rule5))] Gary is white.[(triple9)] Gary is young.[(triple10)] @1: Anne is big.[(((triple2) -> rule3))] Anne is red.[(((triple2) -> rule5))] Dave is red.[(((triple6) -> rule5) OR ((((triple7) -> rule2)) -> rule5))] Gary is nice.[(((triple9) -> rule2))] @2: Anne is cold.[(((((triple2) -> rule3) ((triple2) -> rule5)) -> rule6))] Dave is cold.[(((triple5 ((triple6) -> rule5)) -> rule6) OR ((((triple6) -> rule3) ((triple6) -> rule5)) -> rule6) OR ((triple5 ((((triple7) -> rule2)) -> rule5)) -> rule6) OR ((((triple6) -> rule3) ((((triple7) -> rule2)) -> rule5)) -> rule6) OR ((((((triple7) -> rule2)) -> rule3) ((triple6) -> rule5)) -> rule6) OR ((((((triple7) -> rule2)) -> rule3) ((((triple7) -> rule2)) -> rule5)) -> rule6))] Gary is big.[(((((triple9) -> rule2)) -> rule3))] @3: Anne is white.[(((((((triple2) -> rule3) ((triple2) -> rule5)) -> rule6)) -> rule1))] Gary is cold.[(((((((triple9) -> rule2)) -> rule3) triple8) -> rule6) OR ((((((triple9) -> rule2)) -> rule3) ((((triple9) -> rule2)) -> rule5)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple6) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple7
((((triple5 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((triple6) -> (rule3 % int4)) ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
triple8
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple6) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple9) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule3 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((triple5 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple5 ((((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple6) -> (rule3 % int4)) ((((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((triple7) -> (rule2 % int4))) -> (rule3 % int3)) ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((((triple7) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple7) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((((triple2) -> (rule3 % int4)) ((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple9) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4