Charlie is round. Dave is white. Harry is round. Nice, blue people are not young. If Dave is nice then Dave is big. All white, big people are quiet. If Dave is big and Dave is round then Dave is white. All white people are nice. All big, white people are nice.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
Nice, blue people are not young.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
If Dave is nice then Dave is big.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "big" "+"))
All white, big people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is big and Dave is round then Dave is white.
((("Dave" "is" "big" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "white" "+"))
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
All big, white people are nice.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "round" "-")
triple1
Dave is nice.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "big" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
True
5
proof
[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not quiet.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is round.[(triple1)] Dave is white.[(triple2)] Harry is round.[(triple3)] @1: Dave is nice.[(((triple2) -> rule5))] @2: Dave is big.[(((((triple2) -> rule5)) -> rule2))] @3: Dave is quiet.[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3