Anne is green. Anne is quiet. Anne is smart. Anne is white. Anne is young. Charlie is green. Gary is quiet. If someone is big and smart then they are green. Smart people are white. If Anne is furry and Anne is green then Anne is big. Furry, green people are young. If Charlie is young then Charlie is big. Furry, big people are quiet. If someone is smart and young then they are furry. All furry people are smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is big and smart then they are green.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If Anne is furry and Anne is green then Anne is big.
((("Anne" "is" "furry" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "big" "+"))
Furry, green people are young.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Charlie is young then Charlie is big.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "big" "+"))
Furry, big people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and young then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Anne is quiet.
True
1
proof
[(triple2 OR ((((triple3 triple5) -> rule7) ((((triple3 triple5) -> rule7) triple1) -> rule3)) -> rule6))]
("Anne" "is" "quiet" "+")
triple2
((((triple3 triple5) -> (rule7 % int3)) ((((triple3 triple5) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Charlie is not green.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "green" "-")
triple6
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Charlie" "is" "young" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2 OR ((((triple3 triple5) -> rule7) ((((triple3 triple5) -> rule7) triple1) -> rule3)) -> rule6))] Anne is smart.[(triple3)] Anne is white.[(triple4 OR ((triple3) -> rule2))] Anne is young.[(triple5)] Charlie is green.[(triple6)] Gary is quiet.[(triple7)] @1: Anne is furry.[(((triple3 triple5) -> rule7))] @2: Anne is big.[(((((triple3 triple5) -> rule7) triple1) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((((triple3 triple5) -> (rule7 % int3)) ((((triple3 triple5) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple3 triple5) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple3 triple5) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2