Anne is cold. Anne is furry. Anne is green. Anne is smart. Dave is white. Dave is young. Erin is furry. Erin is smart. Erin is young. Gary is not furry. Gary is kind. Gary is young. Smart things are furry. If Anne is smart then Anne is young. All white things are young. All white things are young. All young things are kind. If something is green and not furry then it is kind. If something is furry and kind then it is white. Kind things are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Anne is smart then Anne is young.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is green and not furry then it is kind.
((("something" "is" "green" "+") ("something" "is" "furry" "~")) -> ("something" "is" "kind" "+"))
If something is furry and kind then it is white.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Dave is young.
True
1
proof
[(triple6 OR ((triple5) -> rule3) OR ((triple5) -> rule4))]
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is furry.
False
1
inv-proof
[(triple10)]
("Gary" "is" "furry" "+")
triple10
Gary is green.
True
2
proof
[(((triple11) -> rule8) OR ((((triple12) -> rule5)) -> rule8))]
("Gary" "is" "green" "+")
((triple11) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not green.
False
2
inv-proof
[(((triple11) -> rule8) OR ((((triple12) -> rule5)) -> rule8))]
("Gary" "is" "green" "-")
((triple11) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is green.
True
3
proof
[(((((triple6) -> rule5)) -> rule8) OR ((((((triple5) -> rule3)) -> rule5)) -> rule8) OR ((((((triple5) -> rule4)) -> rule5)) -> rule8))]
("Dave" "is" "green" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is not white.
False
4
inv-proof
[(((triple7 ((triple9) -> rule5)) -> rule7) OR ((((triple8) -> rule1) ((triple9) -> rule5)) -> rule7))]
("Erin" "is" "white" "-")
((triple7 ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple8) -> (rule1 % int3)) ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Anne is white.
True
5
proof
[(((triple2 ((((triple4) -> rule2)) -> rule5)) -> rule7) OR ((((triple4) -> rule1) ((((triple4) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "white" "+")
((triple2 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not white.
False
5
inv-proof
[(((triple2 ((((triple4) -> rule2)) -> rule5)) -> rule7) OR ((((triple4) -> rule1) ((((triple4) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "white" "-")
((triple2 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2 OR ((triple4) -> rule1))] Anne is green.[(triple3 OR ((((((triple4) -> rule2)) -> rule5)) -> rule8))] Anne is smart.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6 OR ((triple5) -> rule3) OR ((triple5) -> rule4))] Erin is furry.[(triple7 OR ((triple8) -> rule1))] Erin is smart.[(triple8)] Erin is young.[(triple9)] Gary is kind.[(triple11 OR ((triple12) -> rule5))] Gary is not furry.[(triple10)] Gary is young.[(triple12)] @1: Anne is young.[(((triple4) -> rule2))] Dave is kind.[(((triple6) -> rule5) OR ((((triple5) -> rule3)) -> rule5) OR ((((triple5) -> rule4)) -> rule5))] Erin is kind.[(((triple9) -> rule5))] Gary is green.[(((triple11) -> rule8) OR ((((triple12) -> rule5)) -> rule8))] @2: Anne is kind.[(((((triple4) -> rule2)) -> rule5))] Dave is green.[(((((triple6) -> rule5)) -> rule8) OR ((((((triple5) -> rule3)) -> rule5)) -> rule8) OR ((((((triple5) -> rule4)) -> rule5)) -> rule8))] Erin is green.[(((((triple9) -> rule5)) -> rule8))] Erin is white.[(((triple7 ((triple9) -> rule5)) -> rule7) OR ((((triple8) -> rule1) ((triple9) -> rule5)) -> rule7))] @3: Anne is white.[(((triple2 ((((triple4) -> rule2)) -> rule5)) -> rule7) OR ((((triple4) -> rule1) ((((triple4) -> rule2)) -> rule5)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((triple12) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple12
Anne is young.
("Anne" "is" "young" "+")
((triple4) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple6) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple9) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple11) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7 ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple8) -> (rule1 % int3)) ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((triple2 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4