Bob is blue. Bob is rough. Bob is smart. Charlie is big. Charlie is blue. Charlie is green. Charlie is white. If Charlie is green and Charlie is smart then Charlie is rough. Blue things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Charlie is green and Charlie is smart then Charlie is rough.
((("Charlie" "is" "green" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "rough" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Charlie is green.
True
1
proof
[(triple6)]
("Charlie" "is" "green" "+")
triple6
Charlie is not big.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "big" "-")
triple4
Charlie is smart.
True
2
proof
[(((triple5) -> rule2))]
("Charlie" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple5) -> rule2))]
("Charlie" "is" "smart" "-")
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
True
4
proof
[(((triple6 ((triple5) -> rule2)) -> rule1))]
("Charlie" "is" "rough" "+")
((triple6 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple6 ((triple5) -> rule2)) -> rule1))]
("Charlie" "is" "rough" "-")
((triple6 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Bob is smart.[(triple3 OR ((triple1) -> rule2))] Charlie is big.[(triple4)] Charlie is blue.[(triple5)] Charlie is green.[(triple6)] Charlie is white.[(triple7)] @1: Charlie is smart.[(((triple5) -> rule2))] @2: Charlie is rough.[(((triple6 ((triple5) -> rule2)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple6 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2