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