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