Bob is quiet. Bob is red. Bob is rough. Charlie is blue. Charlie is not cold. Charlie is not kind. Erin is blue. Erin is red. Gary is cold. Gary is kind. Gary is quiet. Gary is not young. Kind things are rough. All blue things are rough. If Charlie is rough then Charlie is young. If Gary is cold and Gary is not red then Gary is kind. If Charlie is young and Charlie is blue then Charlie is not quiet. If Erin is young and Erin is rough then Erin is blue.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not young.
("Gary" "is" "young" "-")
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Charlie is rough then Charlie is young.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
If Gary is cold and Gary is not red then Gary is kind.
((("Gary" "is" "cold" "+") ("Gary" "is" "red" "~")) -> ("Gary" "is" "kind" "+"))
If Charlie is young and Charlie is blue then Charlie is not quiet.
((("Charlie" "is" "young" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "-"))
If Erin is young and Erin is rough then Erin is blue.
((("Erin" "is" "young" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "blue" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple9)]
("Gary" "is" "cold" "-")
triple9
Gary is rough.
True
2
proof
[(((triple10) -> rule1))]
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("Gary" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is young.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not quiet.
True
5
proof
[(((((((triple4) -> rule2)) -> rule3) triple4) -> rule5))]
("Charlie" "is" "quiet" "-")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
False
5
inv-proof
[(((((((triple4) -> rule2)) -> rule3) triple4) -> rule5))]
("Charlie" "is" "quiet" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3)] Charlie is blue.[(triple4)] Charlie is not cold.[(triple5)] Charlie is not kind.[(triple6)] Erin is blue.[(triple7)] Erin is red.[(triple8)] Gary is cold.[(triple9)] Gary is kind.[(triple10)] Gary is not young.[(triple12)] Gary is quiet.[(triple11)] @1: Charlie is rough.[(((triple4) -> rule2))] Erin is rough.[(((triple7) -> rule2))] Gary is rough.[(((triple10) -> rule1))] @2: Charlie is young.[(((((triple4) -> rule2)) -> rule3))] @3: Charlie is not quiet.[(((((((triple4) -> rule2)) -> rule3) triple4) -> rule5))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple5
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is not young.
("Gary" "is" "young" "-")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3