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