Anne is young. Bob is young. Charlie is smart. If something is smart then it is not rough. All rough, white things are big. Green, smart things are big. All white things are young. If something is smart and not rough then it is white. Rough things are not white.
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is smart then it is not rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "-"))
All rough, white things are big.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Green, smart things are big.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is smart and not rough then it is white.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "+"))
Rough things are not white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "-"))
Charlie is smart.
True
1
proof
[(triple3)]
("Charlie" "is" "smart" "+")
triple3
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Charlie is not rough.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is rough.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is white.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule5))]
("Charlie" "is" "white" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule5))]
("Charlie" "is" "white" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is young.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule4))]
("Charlie" "is" "young" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
int3
Charlie is not young.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule4))]
("Charlie" "is" "young" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is young.[(triple1)] Bob is young.[(triple2)] Charlie is smart.[(triple3)] @1: Charlie is not rough.[(((triple3) -> rule1))] @2: Charlie is white.[(((triple3 ((triple3) -> rule1)) -> rule5))] @3: Charlie is young.[(((((triple3 ((triple3) -> rule1)) -> rule5)) -> rule4))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
int3