Anne is furry. Charlie is big. Dave is red. Gary is kind. If something is big then it is kind. If something is big then it is kind. If something is white then it is big. If Charlie is furry and Charlie is big then Charlie is young. Kind things are green. All young things are white. Red things are young. All furry, young things are green.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Charlie is furry and Charlie is big then Charlie is young.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "young" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All furry, young things are green.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Gary is not kind.
False
1
inv-proof
[(triple4)]
("Gary" "is" "kind" "-")
triple4
Charlie is kind.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is white.
True
3
proof
[(((((triple3) -> rule7)) -> rule6))]
("Dave" "is" "white" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5) OR ((((triple2) -> rule2)) -> rule5))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is big.
True
4
proof
[(((((((triple3) -> rule7)) -> rule6)) -> rule3))]
("Dave" "is" "big" "+")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule6)) -> rule3))]
("Dave" "is" "big" "-")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@5: Anne is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- rule6 <- rule7 <- FAIL)]]
("Anne" "is" "green" "-")
Gary is big.
Unknown
rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule7 <- FAIL)]]
("Gary" "is" "big" "+")
Anne is not white.
Unknown
inv-rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "young" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Dave is red.[(triple3)] Gary is kind.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule1) OR ((triple2) -> rule2))] Dave is young.[(((triple3) -> rule7))] Gary is green.[(((triple4) -> rule5))] @2: Charlie is green.[(((((triple2) -> rule1)) -> rule5) OR ((((triple2) -> rule2)) -> rule5))] Dave is white.[(((((triple3) -> rule7)) -> rule6))] @3: Dave is big.[(((((((triple3) -> rule7)) -> rule6)) -> rule3))] @4: Dave is kind.[(((((((((triple3) -> rule7)) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple3) -> rule7)) -> rule6)) -> rule3)) -> rule2))] @5: Dave is green.[(((((((((((triple3) -> rule7)) -> rule6)) -> rule3)) -> rule1)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule6)) -> rule3)) -> rule2)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((((((triple3) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((((((((((triple3) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
((((((((((triple3) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5