Anne is big. Anne is smart. Bob is big. Bob is green. Bob is round. Bob is not smart. Bob is white. Bob is young. Dave is green. Dave is not round. Dave is not smart. Gary is big. Gary is green. Gary is smart. Gary is not young. White, smart people are big. All young people are not quiet. Smart people are quiet. If someone is white and big then they are not smart. Round, smart people are not white. If Dave is not young then Dave is white. If Bob is not big then Bob is quiet. All big, quiet people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not young.
("Gary" "is" "young" "-")
White, smart people are big.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All young people are not quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "-"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and big then they are not smart.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "-"))
Round, smart people are not white.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
If Dave is not young then Dave is white.
((("Dave" "is" "young" "~")) -> ("Dave" "is" "white" "+"))
If Bob is not big then Bob is quiet.
((("Bob" "is" "big" "~")) -> ("Bob" "is" "quiet" "+"))
All big, quiet people are green.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Anne is smart.
True
1
proof
[(triple2)]
("Anne" "is" "smart" "+")
triple2
Gary is young.
False
1
inv-proof
[(triple15)]
("Gary" "is" "young" "+")
triple15
Gary is quiet.
True
2
proof
[(((triple14) -> rule3))]
("Gary" "is" "quiet" "+")
((triple14) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Bob is quiet.
False
2
inv-proof
[(((triple8) -> rule2))]
("Bob" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Anne is green.
True
4
proof
[(((triple1 ((triple2) -> rule3)) -> rule8))]
("Anne" "is" "green" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not green.
False
4
inv-proof
[(((triple1 ((triple2) -> rule3)) -> rule8))]
("Anne" "is" "green" "-")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is smart.[(triple2)] Bob is big.[(triple3)] Bob is green.[(triple4)] Bob is not smart.[(triple6 OR ((triple7 triple3) -> rule4))] Bob is round.[(triple5)] Bob is white.[(triple7)] Bob is young.[(triple8)] Dave is green.[(triple9)] Dave is not round.[(triple10)] Dave is not smart.[(triple11)] Gary is big.[(triple12)] Gary is green.[(triple13 OR ((triple12 ((triple14) -> rule3)) -> rule8))] Gary is not young.[(triple15)] Gary is smart.[(triple14)] @1: Anne is quiet.[(((triple2) -> rule3))] Bob is not quiet.[(((triple8) -> rule2))] Gary is quiet.[(((triple14) -> rule3))] @2: Anne is green.[(((triple1 ((triple2) -> rule3)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
((triple7 triple3) -> (rule4 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is not round.
("Dave" "is" "round" "-")
triple10
Dave is not smart.
("Dave" "is" "smart" "-")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is green.
("Gary" "is" "green" "+")
triple13
((triple12 ((triple14) -> (rule3 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple8) -> (rule2 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple14) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2