Anne is furry. Anne is green. Anne is white. Dave is furry. Dave is nice. Dave is round. Dave is white. If someone is nice then they are big. If Anne is green and Anne is furry then Anne is big. Smart people are big. If Dave is white then Dave is smart. Big people are smart. If Anne is white then Anne is nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Anne is green and Anne is furry then Anne is big.
((("Anne" "is" "green" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "big" "+"))
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Dave is white then Dave is smart.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "smart" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Anne is white then Anne is nice.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "nice" "+"))
Dave is white.
True
1
proof
[(triple7)]
("Dave" "is" "white" "+")
triple7
Anne is not white.
False
1
inv-proof
[(triple3)]
("Anne" "is" "white" "-")
triple3
Dave is smart.
True
2
proof
[(((triple7) -> rule4) OR ((((triple5) -> rule1)) -> rule5))]
("Dave" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Anne is not big.
False
3
inv-proof
[(((triple2 triple1) -> rule2) OR ((((triple3) -> rule6)) -> rule1))]
("Anne" "is" "big" "-")
((triple2 triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is white.[(triple3)] Dave is furry.[(triple4)] Dave is nice.[(triple5)] Dave is round.[(triple6)] Dave is white.[(triple7)] @1: Anne is big.[(((triple2 triple1) -> rule2) OR ((((triple3) -> rule6)) -> rule1))] Anne is nice.[(((triple3) -> rule6))] Dave is big.[(((triple5) -> rule1) OR ((((triple7) -> rule4)) -> rule3))] Dave is smart.[(((triple7) -> rule4) OR ((((triple5) -> rule1)) -> rule5))] @2: Anne is smart.[(((((triple2 triple1) -> rule2)) -> rule5) OR ((((((triple3) -> rule6)) -> rule1)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3