Bob is quiet. Charlie is kind. Charlie is white. If something is kind then it is quiet. If something is nice and big then it is quiet. If Charlie is young then Charlie is white. If Bob is kind and Bob is blue then Bob is big. All white, blue things are young. White, quiet things are nice. Kind, blue things are white. All white, nice things are young.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is nice and big then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is young then Charlie is white.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "white" "+"))
If Bob is kind and Bob is blue then Bob is big.
((("Bob" "is" "kind" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "big" "+"))
All white, blue things are young.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
White, quiet things are nice.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Kind, blue things are white.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All white, nice things are young.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Charlie is not white.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "white" "-")
triple3
Charlie is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
True
4
proof
[(((triple3 ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "nice" "+")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((triple3 ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "nice" "-")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
True
6
proof
[(((triple3 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule8))]
("Charlie" "is" "young" "+")
((triple3 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not young.
False
6
inv-proof
[(((triple3 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule8))]
("Charlie" "is" "young" "-")
((triple3 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is quiet.[(triple1)] Charlie is kind.[(triple2)] Charlie is white.[(triple3)] @1: Charlie is quiet.[(((triple2) -> rule1))] @2: Charlie is nice.[(((triple3 ((triple2) -> rule1)) -> rule6))] @3: Charlie is young.[(((triple3 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule8))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple3 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3