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