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