Fiona is young. Gary is nice. Gary is white. If something is smart and round then it is cold. All round, nice things are smart. All white, smart things are round. Nice things are white. If Gary is round and Gary is cold then Gary is white. White things are round.
Fiona is young.
("Fiona" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is smart and round then it is cold.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All round, nice things are smart.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All white, smart things are round.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Gary is round and Gary is cold then Gary is white.
((("Gary" "is" "round" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Gary is white.
True
1
proof
[(triple3 OR ((triple2) -> rule4))]
("Gary" "is" "white" "+")
triple3
((triple2) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule4))]
("Gary" "is" "white" "-")
triple3
((triple2) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
True
2
proof
[(((triple3) -> rule6) OR ((((triple2) -> rule4)) -> rule6))]
("Gary" "is" "round" "+")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not round.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple2) -> rule4)) -> rule6))]
("Gary" "is" "round" "-")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is cold.
Unknown
rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "cold" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Fiona is young.[(triple1)] Gary is nice.[(triple2)] Gary is white.[(triple3 OR ((triple2) -> rule4))] @1: Gary is round.[(((triple3) -> rule6) OR ((((triple2) -> rule4)) -> rule6))] @2: Gary is smart.[(((((triple3) -> rule6) triple2) -> rule2) OR ((((((triple2) -> rule4)) -> rule6) triple2) -> rule2))] @3: Gary is cold.[(((((((triple3) -> rule6) triple2) -> rule2) ((triple3) -> rule6)) -> rule1) OR ((((((triple3) -> rule6) triple2) -> rule2) ((((triple2) -> rule4)) -> rule6)) -> rule1) OR ((((((((triple2) -> rule4)) -> rule6) triple2) -> rule2) ((triple3) -> rule6)) -> rule1) OR ((((((((triple2) -> rule4)) -> rule6) triple2) -> rule2) ((((triple2) -> rule4)) -> rule6)) -> rule1))]
Fiona is young.
("Fiona" "is" "young" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
((triple2) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((triple3) -> (rule6 % int3))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple3) -> (rule6 % int4)) triple2) -> (rule2 % int3)) ((((triple2) -> (rule4 % int2))) -> (rule6 % int4))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((((((((triple2) -> (rule4 % int4))) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((triple3) -> (rule6 % int3))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple2) -> (rule4 % int4))) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4