Charlie is blue. Charlie is not furry. Dave is nice. Erin is big. Fiona is nice. Fiona is quiet. Fiona is rough. All nice, blue people are furry. If Dave is nice then Dave is blue. If someone is furry and blue then they are big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All nice, blue people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Dave is nice then Dave is blue.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "blue" "+"))
If someone is furry and blue then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Fiona is rough.
True
1
proof
[(triple7)]
("Fiona" "is" "rough" "+")
triple7
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Dave is blue.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Dave" "is" "furry" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Dave" "is" "furry" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
True
7
proof
[(((((triple3 ((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not big.
False
7
inv-proof
[(((((triple3 ((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Charlie is blue.[(triple1)] Charlie is not furry.[(triple2)] Dave is nice.[(triple3)] Erin is big.[(triple4)] Fiona is nice.[(triple5)] Fiona is quiet.[(triple6)] Fiona is rough.[(triple7)] @1: Dave is blue.[(((triple3) -> rule2))] @2: Dave is furry.[(((triple3 ((triple3) -> rule2)) -> rule1))] @3: Dave is big.[(((((triple3 ((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3