Anne is nice. Charlie is big. Dave is quiet. Harry is big. White, nice people are red. Quiet people are white. Big, blue people are red. If Anne is quiet then Anne is big. Nice people are quiet. All big people are nice.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
White, nice people are red.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Big, blue people are red.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Anne is quiet then Anne is big.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "big" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Charlie is nice.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
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 not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Charlie is big.[(triple2)] Dave is quiet.[(triple3)] Harry is big.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule5))] Charlie is nice.[(((triple2) -> rule6))] Dave is white.[(((triple3) -> rule2))] Harry is nice.[(((triple4) -> rule6))] @2: Anne is big.[(((((triple1) -> rule5)) -> rule4))] Anne is white.[(((((triple1) -> rule5)) -> rule2))] Charlie is quiet.[(((((triple2) -> rule6)) -> rule5))] Harry is quiet.[(((((triple4) -> rule6)) -> rule5))] @3: Anne is red.[(((((((triple1) -> rule5)) -> rule2) triple1) -> rule1))] Charlie is white.[(((((((triple2) -> rule6)) -> rule5)) -> rule2))] Harry is white.[(((((((triple4) -> rule6)) -> rule5)) -> rule2))] @4: Charlie is red.[(((((((((triple2) -> rule6)) -> rule5)) -> rule2) ((triple2) -> rule6)) -> rule1))] Harry is red.[(((((((((triple4) -> rule6)) -> rule5)) -> rule2) ((triple4) -> rule6)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int4))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((((((((triple4) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple4) -> (rule6 % int4))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4