Charlie is big. Charlie is blue. Charlie is kind. Charlie is young. Dave is not big. Dave is blue. Dave is not furry. Dave is kind. Gary is not big. Gary is kind. Gary is not quiet. Gary is red. All furry people are big. All red, blue people are quiet. If Charlie is young and Charlie is kind then Charlie is quiet. Furry, quiet people are kind. All young people are kind. If someone is blue and not big then they are red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All red, blue people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is young and Charlie is kind then Charlie is quiet.
((("Charlie" "is" "young" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
Furry, quiet people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and not big then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple4) -> rule5))]
("Charlie" "is" "kind" "+")
triple3
((triple4) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is not kind.
False
1
inv-proof
[(triple8)]
("Dave" "is" "kind" "-")
triple8
Dave is red.
True
3
proof
[(((triple6 triple5) -> rule6))]
("Dave" "is" "red" "+")
((triple6 triple5) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple6 triple5) -> rule6))]
("Dave" "is" "red" "-")
((triple6 triple5) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
True
5
proof
[(((((triple6 triple5) -> rule6) triple6) -> rule2))]
("Dave" "is" "quiet" "+")
((((triple6 triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not quiet.
False
5
inv-proof
[(((((triple6 triple5) -> rule6) triple6) -> rule2))]
("Dave" "is" "quiet" "-")
((((triple6 triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is kind.[(triple3 OR ((triple4) -> rule5))] Charlie is young.[(triple4)] Dave is blue.[(triple6)] Dave is kind.[(triple8)] Dave is not big.[(triple5)] Dave is not furry.[(triple7)] Gary is kind.[(triple10)] Gary is not big.[(triple9)] Gary is not quiet.[(triple11)] Gary is red.[(triple12)] @1: Charlie is quiet.[(((triple4 triple3) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule3))] Dave is red.[(((triple6 triple5) -> rule6))] @2: Dave is quiet.[(((((triple6 triple5) -> rule6) triple6) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple4) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is not big.
("Dave" "is" "big" "-")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is not big.
("Gary" "is" "big" "-")
triple9
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 triple3) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple4 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple6 triple5) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple6 triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2