Anne is white. Anne is young. Bob is rough. Bob is not smart. Charlie is not green. Charlie is kind. Charlie is smart. If someone is white then they are green. Kind people are young. If Anne is green then Anne is smart. Green, kind people are rough. If someone is smart and not green then they are rough. Green people are not rough. If someone is white and not rough then they are blue. Rough, kind people are blue.
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Anne is green then Anne is smart.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "smart" "+"))
Green, kind people are rough.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and not green then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "rough" "+"))
Green people are not rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "-"))
If someone is white and not rough then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "blue" "+"))
Rough, kind people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
Charlie is young.
True
2
proof
[(((triple6) -> rule2))]
("Charlie" "is" "young" "+")
((triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is not blue.
False
5
inv-proof
[(((((triple7 triple5) -> rule5) triple6) -> rule8))]
("Charlie" "is" "blue" "-")
((((triple7 triple5) -> (rule5 % int2)) triple6) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is white.[(triple1)] Anne is young.[(triple2)] Bob is not smart.[(triple4)] Bob is rough.[(triple3)] Charlie is kind.[(triple6)] Charlie is not green.[(triple5)] Charlie is smart.[(triple7)] @1: Anne is green.[(((triple1) -> rule1))] Charlie is rough.[(((triple7 triple5) -> rule5))] Charlie is young.[(((triple6) -> rule2))] @2: Anne is not rough.[(((((triple1) -> rule1)) -> rule6))] Anne is smart.[(((((triple1) -> rule1)) -> rule3))] Charlie is blue.[(((((triple7 triple5) -> rule5) triple6) -> rule8))] @3: Anne is blue.[(((triple1 ((((triple1) -> rule1)) -> rule6)) -> rule7))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is not green.
("Charlie" "is" "green" "-")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7 triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple7 triple5) -> (rule5 % int2)) triple6) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
int2
Anne is green.
("Anne" "is" "green" "+")
int3