Bob is red. Charlie is big. If something is red and smart then it is young. Quiet, red things are rough. All big things are quiet. If Charlie is kind and Charlie is red then Charlie is rough. All smart, kind things are big. All quiet things are rough.
Bob is red.
("Bob" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
If something is red and smart then it is young.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Quiet, red things are rough.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is kind and Charlie is red then Charlie is rough.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "rough" "+"))
All smart, kind things are big.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is red.[(triple1)] Charlie is big.[(triple2)] @1: Charlie is quiet.[(((triple2) -> rule3))] @2: Charlie is rough.[(((((triple2) -> rule3)) -> rule6))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2