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