Dave is quiet. Fiona is cold. Gary is round. Round, white people are big. If someone is quiet then they are round. If someone is green then they are not kind. If someone is big and green then they are cold. If someone is big and green then they are not cold. If someone is big and not round then they are cold. Big, cold people are green. If someone is round and quiet then they are green.
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Round, white people are big.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is green then they are not kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "-"))
If someone is big and green then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is big and green then they are not cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
If someone is big and not round then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "+"))
Big, cold people are green.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is round and quiet then they are green.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Dave is round.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "round" "-")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule8))]
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule8))]
("Dave" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule8)) -> rule3))]
("Dave" "is" "kind" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule8)) -> rule3))]
("Dave" "is" "kind" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Dave is quiet.[(triple1)] Fiona is cold.[(triple2)] Gary is round.[(triple3)] @1: Dave is round.[(((triple1) -> rule2))] @2: Dave is green.[(((((triple1) -> rule2) triple1) -> rule8))] @3: Dave is not kind.[(((((((triple1) -> rule2) triple1) -> rule8)) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3