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