Charlie is big. Charlie is blue. Charlie is white. Erin is cold. Fiona is blue. Fiona is red. Fiona is white. Gary is big. Gary is blue. Gary is cold. Gary is red. Gary is white. White people are red. All quiet, red people are not cold. All big people are cold. If Erin is cold and Erin is not white then Erin is not smart. All smart people are quiet. If someone is smart and not red then they are not quiet. If someone is smart and white then they are big. If someone is white then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All quiet, red people are not cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "-"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Erin is cold and Erin is not white then Erin is not smart.
((("Erin" "is" "cold" "+") ("Erin" "is" "white" "~")) -> ("Erin" "is" "smart" "-"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and not red then they are not quiet.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "quiet" "-"))
If someone is smart and white then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Gary is white.
True
1
proof
[(triple12)]
("Gary" "is" "white" "+")
triple12
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Charlie is cold.
True
2
proof
[(((triple1) -> rule3) OR ((((triple3) -> rule8)) -> rule3))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is not big.
False
2
inv-proof
[(((triple7) -> rule8))]
("Fiona" "is" "big" "-")
((triple7) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("Fiona" "is" "cold" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule3))]
("Fiona" "is" "cold" "-")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Charlie is big.[(triple1 OR ((triple3) -> rule8))] Charlie is blue.[(triple2)] Charlie is white.[(triple3)] Erin is cold.[(triple4)] Fiona is blue.[(triple5)] Fiona is red.[(triple6 OR ((triple7) -> rule1))] Fiona is white.[(triple7)] Gary is big.[(triple8 OR ((triple12) -> rule8))] Gary is blue.[(triple9)] Gary is cold.[(triple10 OR ((triple8) -> rule3) OR ((((triple12) -> rule8)) -> rule3))] Gary is red.[(triple11 OR ((triple12) -> rule1))] Gary is white.[(triple12)] @1: Charlie is cold.[(((triple1) -> rule3) OR ((((triple3) -> rule8)) -> rule3))] Charlie is red.[(((triple3) -> rule1))] Fiona is big.[(((triple7) -> rule8))] @2: Fiona is cold.[(((((triple7) -> rule8)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
((triple7) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple12) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((triple8) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple12) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2