Dave is nice. Dave is quiet. Dave is red. Gary is furry. Gary is nice. Harry is red. Harry is young. If Dave is not red then Dave is green. If something is young and not nice then it is quiet. If something is green and young then it is quiet. If something is nice then it is green. If something is nice and green then it is young. If Harry is green then Harry is not furry.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is not red then Dave is green.
((("Dave" "is" "red" "~")) -> ("Dave" "is" "green" "+"))
If something is young and not nice then it is quiet.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If something is green and young then it is quiet.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice and green then it is young.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Harry is green then Harry is not furry.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "furry" "-"))
Dave is red.
True
1
proof
[(triple3)]
("Dave" "is" "red" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Dave is green.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "-")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule5))]
("Dave" "is" "young" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple5 ((triple5) -> rule4)) -> rule5))]
("Gary" "is" "young" "-")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
True
7
proof
[(((((triple5) -> rule4) ((triple5 ((triple5) -> rule4)) -> rule5)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple5) -> (rule4 % int3)) ((triple5 ((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not quiet.
False
7
inv-proof
[(((((triple5) -> rule4) ((triple5 ((triple5) -> rule4)) -> rule5)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple5) -> (rule4 % int3)) ((triple5 ((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is nice.[(triple1)] Dave is quiet.[(triple2 OR ((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule5)) -> rule3))] Dave is red.[(triple3)] Gary is furry.[(triple4)] Gary is nice.[(triple5)] Harry is red.[(triple6)] Harry is young.[(triple7)] @1: Dave is green.[(((triple1) -> rule4))] Gary is green.[(((triple5) -> rule4))] @2: Dave is young.[(((triple1 ((triple1) -> rule4)) -> rule5))] Gary is young.[(((triple5 ((triple5) -> rule4)) -> rule5))] @3: Gary is quiet.[(((((triple5) -> rule4) ((triple5 ((triple5) -> rule4)) -> rule5)) -> rule3))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple5) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple5) -> (rule4 % int3)) ((triple5 ((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3