Dave is blue. Fiona is blue. Gary is quiet. If Fiona is white and Fiona is blue then Fiona is not smart. All big, smart people are white. If someone is quiet then they are white. If someone is cold and not nice then they are white. If someone is blue then they are not quiet. If someone is smart and not nice then they are quiet. If someone is nice and big then they are cold. All white people are big.
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Fiona is white and Fiona is blue then Fiona is not smart.
((("Fiona" "is" "white" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "smart" "-"))
All big, smart people are white.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and not nice then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "white" "+"))
If someone is blue then they are not quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "-"))
If someone is smart and not nice then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
If someone is nice and big then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Dave is not quiet.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "white" "-")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
True
3
proof
[(((((triple3) -> rule3)) -> rule8))]
("Gary" "is" "big" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule8))]
("Gary" "is" "big" "-")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Dave is blue.[(triple1)] Fiona is blue.[(triple2)] Gary is quiet.[(triple3)] @1: Dave is not quiet.[(((triple1) -> rule5))] Fiona is not quiet.[(((triple2) -> rule5))] Gary is white.[(((triple3) -> rule3))] @2: Gary is big.[(((((triple3) -> rule3)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2