Anne is nice. Anne is red. Dave is furry. Dave is young. Fiona is big. Harry is nice. Harry is not white. If Dave is white then Dave is big. All furry people are white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not white.
("Harry" "is" "white" "-")
If Dave is white then Dave is big.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "big" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Dave is young.
True
1
proof
[(triple4)]
("Dave" "is" "young" "+")
triple4
Harry is not nice.
False
1
inv-proof
[(triple6)]
("Harry" "is" "nice" "-")
triple6
Dave is white.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "white" "-")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "big" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "white" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Dave is furry.[(triple3)] Dave is young.[(triple4)] Fiona is big.[(triple5)] Harry is nice.[(triple6)] Harry is not white.[(triple7)] @1: Dave is white.[(((triple3) -> rule2))] @2: Dave is big.[(((((triple3) -> rule2)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is not white.
("Harry" "is" "white" "-")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2