Charlie is smart. Fiona is smart. Gary is round. Round, smart things are white. All smart things are round. If Fiona is not red and Fiona is not smart then Fiona is round. If something is smart and round then it is green. Red things are green. If something is white and not smart then it is not quiet.
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
Round, smart things are white.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Fiona is not red and Fiona is not smart then Fiona is round.
((("Fiona" "is" "red" "~") ("Fiona" "is" "smart" "~")) -> ("Fiona" "is" "round" "+"))
If something is smart and round then it is green.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is white and not smart then it is not quiet.
((("something" "is" "white" "+") ("something" "is" "smart" "~")) -> ("something" "is" "quiet" "-"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Fiona is round.
True
2
proof
[(((triple2) -> rule2))]
("Fiona" "is" "round" "+")
((triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "round" "-")
((triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule4))]
("Fiona" "is" "green" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Charlie is smart.[(triple1)] Fiona is smart.[(triple2)] Gary is round.[(triple3)] @1: Charlie is round.[(((triple1) -> rule2))] Fiona is round.[(((triple2) -> rule2))] @2: Charlie is green.[(((triple1 ((triple1) -> rule2)) -> rule4))] Charlie is white.[(((((triple1) -> rule2) triple1) -> rule1))] Fiona is green.[(((triple2 ((triple2) -> rule2)) -> rule4))] Fiona is white.[(((((triple2) -> rule2) triple2) -> rule1))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2