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