Bob is blue. Charlie is blue. If Bob is quiet and Bob is young then Bob is kind. If Charlie is green then Charlie is white. Kind people are green. All blue people are kind. Green, quiet people are white. If someone is smart then they are young.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
If Bob is quiet and Bob is young then Bob is kind.
((("Bob" "is" "quiet" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "kind" "+"))
If Charlie is green then Charlie is white.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "white" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Green, quiet people are white.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "young" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Charlie is blue.[(triple2)] @1: Bob is kind.[(((triple1) -> rule4))] Charlie is kind.[(((triple2) -> rule4))] @2: Bob is green.[(((((triple1) -> rule4)) -> rule3))] Charlie is green.[(((((triple2) -> rule4)) -> rule3))] @3: Charlie is white.[(((((((triple2) -> rule4)) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3