Charlie is nice. Fiona is round. Gary is white. Harry is round. White things are cold. All white, red things are round. All cold things are red.
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All white, red things are round.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Gary is cold.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "red" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule3)) -> rule2))]
("Gary" "is" "round" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not round.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule3)) -> rule2))]
("Gary" "is" "round" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is nice.[(triple1)] Fiona is round.[(triple2)] Gary is white.[(triple3)] Harry is round.[(triple4)] @1: Gary is cold.[(((triple3) -> rule1))] @2: Gary is red.[(((((triple3) -> rule1)) -> rule3))] @3: Gary is round.[(((triple3 ((((triple3) -> rule1)) -> rule3)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3