Charlie is white. Dave is quiet. Erin is quiet. Gary is cold. All big things are cold. All white things are red. Quiet, red things are white. If something is big then it is quiet. If Gary is big and Gary is blue then Gary is smart. White, cold things are blue. If something is quiet then it is white. If Erin is smart and Erin is quiet then Erin is blue.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Quiet, red things are white.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Gary is big and Gary is blue then Gary is smart.
((("Gary" "is" "big" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "smart" "+"))
White, cold things are blue.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If Erin is smart and Erin is quiet then Erin is blue.
((("Erin" "is" "smart" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "blue" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Erin is white.
True
2
proof
[(((triple3) -> rule7))]
("Erin" "is" "white" "+")
((triple3) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule7))]
("Dave" "is" "white" "-")
((triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is red.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("Erin" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule2))]
("Erin" "is" "red" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is white.[(triple1)] Dave is quiet.[(triple2)] Erin is quiet.[(triple3)] Gary is cold.[(triple4)] @1: Charlie is red.[(((triple1) -> rule2))] Dave is white.[(((triple2) -> rule7))] Erin is white.[(((triple3) -> rule7))] @2: Dave is red.[(((((triple2) -> rule7)) -> rule2))] Erin is red.[(((((triple3) -> rule7)) -> rule2))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2