Anne is blue. Anne is nice. Anne is young. Charlie is big. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is white. Charlie is young. Dave is blue. Dave is furry. Dave is nice. Dave is round. Harry is big. Harry is nice. Harry is young. If Dave is nice and Dave is blue then Dave is big. All round, white people are big.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is nice and Dave is blue then Dave is big.
((("Dave" "is" "nice" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "big" "+"))
All round, white people are big.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Dave is furry.
True
1
proof
[(triple11)]
("Dave" "is" "furry" "+")
triple11
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Dave is big.
True
3
proof
[(((triple12 triple10) -> rule1))]
("Dave" "is" "big" "+")
((triple12 triple10) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
3
inv-proof
[(((triple12 triple10) -> rule1))]
("Dave" "is" "big" "-")
((triple12 triple10) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is young.[(triple3)] Charlie is big.[(triple4)] Charlie is blue.[(triple5)] Charlie is furry.[(triple6)] Charlie is nice.[(triple7)] Charlie is white.[(triple8)] Charlie is young.[(triple9)] Dave is blue.[(triple10)] Dave is furry.[(triple11)] Dave is nice.[(triple12)] Dave is round.[(triple13)] Harry is big.[(triple14)] Harry is nice.[(triple15)] Harry is young.[(triple16)] @1: Dave is big.[(((triple12 triple10) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple9
Dave is blue.
("Dave" "is" "blue" "+")
triple10
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is round.
("Dave" "is" "round" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Dave is big.
("Dave" "is" "big" "+")
((triple12 triple10) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1