Bob is green. All smart things are green. If something is kind then it is rough. All young, rough things are kind. If Bob is green then Bob is smart. Green things are kind. If something is young then it is smart. If something is kind and young then it is green. Young things are rough.
Bob is green.
("Bob" "is" "green" "+")
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All young, rough things are kind.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Bob is green then Bob is smart.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is kind and young then it is green.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Bob is kind.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is green.[(triple1)] @1: Bob is kind.[(((triple1) -> rule5))] Bob is smart.[(((triple1) -> rule4))] @2: Bob is rough.[(((((triple1) -> rule5)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2