Charlie is big. Charlie is cold. Charlie is green. Charlie is quiet. Charlie is white. Charlie is young. Dave is quiet. Fiona is cold. Gary is cold. Gary is white. All white people are cold. White people are red. If someone is red and cold then they are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is red and cold then they are young.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Charlie is cold.
True
1
proof
[(triple2 OR ((triple5) -> rule1))]
("Charlie" "is" "cold" "+")
triple2
((triple5) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple7)]
("Dave" "is" "quiet" "-")
triple7
Gary is red.
True
2
proof
[(((triple10) -> rule2))]
("Gary" "is" "red" "+")
((triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple5) -> rule2))]
("Charlie" "is" "red" "-")
((triple5) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is young.
True
4
proof
[(((((triple10) -> rule2) triple9) -> rule3) OR ((((triple10) -> rule2) ((triple10) -> rule1)) -> rule3))]
("Gary" "is" "young" "+")
((((triple10) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not young.
False
4
inv-proof
[(((((triple10) -> rule2) triple9) -> rule3) OR ((((triple10) -> rule2) ((triple10) -> rule1)) -> rule3))]
("Gary" "is" "young" "-")
((((triple10) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2 OR ((triple5) -> rule1))] Charlie is green.[(triple3)] Charlie is quiet.[(triple4)] Charlie is white.[(triple5)] Charlie is young.[(triple6 OR ((((triple5) -> rule2) triple2) -> rule3) OR ((((triple5) -> rule2) ((triple5) -> rule1)) -> rule3))] Dave is quiet.[(triple7)] Fiona is cold.[(triple8)] Gary is cold.[(triple9 OR ((triple10) -> rule1))] Gary is white.[(triple10)] @1: Charlie is red.[(((triple5) -> rule2))] Gary is red.[(((triple10) -> rule2))] @2: Gary is young.[(((((triple10) -> rule2) triple9) -> rule3) OR ((((triple10) -> rule2) ((triple10) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple5) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((((triple5) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple10) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple10) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3