Bob is rough. Charlie is cold. Erin is cold. Erin is kind. Gary is cold. Gary is not green. Gary is kind. All kind people are quiet. All big people are quiet. If Charlie is kind then Charlie is rough. Cold people are kind. All quiet people are cold. All quiet, kind people are red. If someone is red and not kind then they are not rough. If someone is kind and not red then they are rough.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is kind then Charlie is rough.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "rough" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is red and not kind then they are not rough.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "-"))
If someone is kind and not red then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "rough" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Gary is not cold.
False
1
inv-proof
[(triple5 OR ((((triple7) -> rule1)) -> rule5))]
("Gary" "is" "cold" "-")
triple5
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
True
2
proof
[(((triple7) -> rule1) OR ((((triple5) -> rule4)) -> rule1))]
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple7) -> rule1) triple7) -> rule6) OR ((((triple7) -> rule1) ((triple5) -> rule4)) -> rule6) OR ((((((triple5) -> rule4)) -> rule1) triple7) -> rule6) OR ((((((triple5) -> rule4)) -> rule1) ((triple5) -> rule4)) -> rule6))]
("Gary" "is" "red" "-")
((((triple7) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2)) ((triple5) -> (rule4 % int3))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Charlie is red.
True
6
proof
[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))]
("Charlie" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not red.
False
6
inv-proof
[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))]
("Charlie" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "rough" "-")
Bob is cold.
Unknown
rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not kind.
Unknown
inv-rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is rough.[(triple1)] Charlie is cold.[(triple2)] Erin is cold.[(triple3 OR ((((triple4) -> rule1)) -> rule5))] Erin is kind.[(triple4 OR ((triple3) -> rule4))] Gary is cold.[(triple5 OR ((((triple7) -> rule1)) -> rule5))] Gary is kind.[(triple7 OR ((triple5) -> rule4))] Gary is not green.[(triple6)] @1: Charlie is kind.[(((triple2) -> rule4))] Erin is quiet.[(((triple4) -> rule1) OR ((((triple3) -> rule4)) -> rule1))] Gary is quiet.[(((triple7) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] @2: Charlie is quiet.[(((((triple2) -> rule4)) -> rule1))] Charlie is rough.[(((((triple2) -> rule4)) -> rule3))] Erin is red.[(((((triple4) -> rule1) triple4) -> rule6) OR ((((triple4) -> rule1) ((triple3) -> rule4)) -> rule6) OR ((((((triple3) -> rule4)) -> rule1) triple4) -> rule6) OR ((((((triple3) -> rule4)) -> rule1) ((triple3) -> rule4)) -> rule6))] Gary is red.[(((((triple7) -> rule1) triple7) -> rule6) OR ((((triple7) -> rule1) ((triple5) -> rule4)) -> rule6) OR ((((((triple5) -> rule4)) -> rule1) triple7) -> rule6) OR ((((((triple5) -> rule4)) -> rule1) ((triple5) -> rule4)) -> rule6))] @3: Charlie is red.[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple3) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple5) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2)) ((triple5) -> (rule4 % int3))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3