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