Anne is blue. Anne is furry. Anne is red. Anne is young. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is red. Charlie is round. Charlie is young. Dave is blue. Dave is furry. Dave is nice. Dave is red. Dave is round. If Charlie is blue then Charlie is nice. If something is furry and nice then it is round. Young things are blue. If something is young then it is nice. If something is red and nice then it is white. All red, white things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
If Charlie is blue then Charlie is nice.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "nice" "+"))
If something is furry and nice then it is round.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is red and nice then it is white.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
All red, white things are blue.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Dave is furry.
True
1
proof
[(triple12)]
("Dave" "is" "furry" "+")
triple12
Charlie is not red.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "red" "-")
triple8
@0: Anne is blue.[(triple1 OR ((triple4) -> rule3) OR ((triple3 ((triple3 ((triple4) -> rule4)) -> rule5)) -> rule6))] Anne is furry.[(triple2)] Anne is red.[(triple3)] Anne is young.[(triple4)] Charlie is blue.[(triple5 OR ((triple10) -> rule3) OR ((triple8 ((triple8 triple7) -> rule5)) -> rule6) OR ((triple8 ((triple8 ((triple10) -> rule4)) -> rule5)) -> rule6))] Charlie is furry.[(triple6)] Charlie is nice.[(triple7 OR ((triple10) -> rule4) OR ((triple5) -> rule1) OR ((((triple10) -> rule3)) -> rule1))] Charlie is red.[(triple8)] Charlie is round.[(triple9 OR ((triple6 triple7) -> rule2) OR ((triple6 ((triple10) -> rule4)) -> rule2) OR ((triple6 ((triple5) -> rule1)) -> rule2) OR ((triple6 ((((triple10) -> rule3)) -> rule1)) -> rule2))] Charlie is young.[(triple10)] Dave is blue.[(triple11 OR ((triple14 ((triple14 triple13) -> rule5)) -> rule6))] Dave is furry.[(triple12)] Dave is nice.[(triple13)] Dave is red.[(triple14)] Dave is round.[(triple15 OR ((triple12 triple13) -> rule2))] @1: Anne is nice.[(((triple4) -> rule4))] Charlie is white.[(((triple8 triple7) -> rule5) OR ((triple8 ((triple10) -> rule4)) -> rule5) OR ((triple8 ((triple5) -> rule1)) -> rule5) OR ((triple8 ((((triple10) -> rule3)) -> rule1)) -> rule5))] Dave is white.[(((triple14 triple13) -> rule5))] @2: Anne is round.[(((triple2 ((triple4) -> rule4)) -> rule2))] Anne is white.[(((triple3 ((triple4) -> rule4)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3 ((triple3 ((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple10) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple8 ((triple8 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple8 ((triple8 ((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple10) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple5) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
((triple6 triple7) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple6 ((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple6 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple6 ((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
triple11
((triple14 ((triple14 triple13) -> (rule5 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
triple13
Dave is red.
("Dave" "is" "red" "+")
triple14
Dave is round.
("Dave" "is" "round" "+")
triple15
((triple12 triple13) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8 triple7) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple8 ((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple8 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple8 ((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple14 triple13) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2 ((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple3 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2