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