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