Bob is big. Bob is green. Bob is kind. Erin is big. Erin is green. Erin is nice. Gary is not quiet. If Gary is nice then Gary is cold. Young things are quiet. If something is kind and green then it is quiet. All quiet things are big. If something is green then it is kind. If something is nice and not kind then it is not cold. If something is quiet and not green then it is not cold. All quiet things are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
If Gary is nice then Gary is cold.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "cold" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and green then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is green then it is kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is nice and not kind then it is not cold.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "-"))
If something is quiet and not green then it is not cold.
((("something" "is" "quiet" "+") ("something" "is" "green" "~")) -> ("something" "is" "cold" "-"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Erin is big.
True
1
proof
[(triple4 OR ((((((triple5) -> rule5) triple5) -> rule3)) -> rule4))]
("Erin" "is" "big" "+")
triple4
((((((triple5) -> (rule5 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not green.
False
1
inv-proof
[(triple5)]
("Erin" "is" "green" "-")
triple5
Erin is kind.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "kind" "+")
((triple5) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple5) -> rule5))]
("Erin" "is" "kind" "-")
((triple5) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple5) -> rule5) triple5) -> rule3))]
("Erin" "is" "quiet" "+")
((((triple5) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple3 triple2) -> rule3)) -> rule8) OR ((((((triple2) -> rule5) triple2) -> rule3)) -> rule8))]
("Bob" "is" "cold" "-")
((((triple3 triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is cold.
True
5
proof
[(((((((triple5) -> rule5) triple5) -> rule3)) -> rule8))]
("Erin" "is" "cold" "+")
((((((triple5) -> (rule5 % int3)) triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((((((triple5) -> rule5) triple5) -> rule3)) -> rule8))]
("Erin" "is" "cold" "-")
((((((triple5) -> (rule5 % int3)) triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Bob is big.[(triple1 OR ((((triple3 triple2) -> rule3)) -> rule4) OR ((((((triple2) -> rule5) triple2) -> rule3)) -> rule4))] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule5))] Erin is big.[(triple4 OR ((((((triple5) -> rule5) triple5) -> rule3)) -> rule4))] Erin is green.[(triple5)] Erin is nice.[(triple6)] Gary is not quiet.[(triple7)] @1: Bob is quiet.[(((triple3 triple2) -> rule3) OR ((((triple2) -> rule5) triple2) -> rule3))] Erin is kind.[(((triple5) -> rule5))] @2: Bob is cold.[(((((triple3 triple2) -> rule3)) -> rule8) OR ((((((triple2) -> rule5) triple2) -> rule3)) -> rule8))] Erin is quiet.[(((((triple5) -> rule5) triple5) -> rule3))] @3: Erin is cold.[(((((((triple5) -> rule5) triple5) -> rule3)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple3 triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple4
((((((triple5) -> (rule5 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple5) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple5) -> (rule5 % int3)) triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3