Bob is red. Charlie is not green. Fiona is red. Harry is round. All red people are cold. Quiet, cold people are not red. If Charlie is green then Charlie is quiet. If Fiona is round then Fiona is green. If Harry is not green and Harry is not red then Harry is round. If someone is nice then they are round. All cold people are round. If someone is red and not quiet then they are round.
Bob is red.
("Bob" "is" "red" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Quiet, cold people are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "-"))
If Charlie is green then Charlie is quiet.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "quiet" "+"))
If Fiona is round then Fiona is green.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "green" "+"))
If Harry is not green and Harry is not red then Harry is round.
((("Harry" "is" "green" "~") ("Harry" "is" "red" "~")) -> ("Harry" "is" "round" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is red and not quiet then they are round.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "round" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "red" "-")
triple3
Fiona is cold.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is round.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("Fiona" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("Fiona" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
True
4
proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule4))]
("Fiona" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not green.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule4))]
("Fiona" "is" "green" "-")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is red.[(triple1)] Charlie is not green.[(triple2)] Fiona is red.[(triple3)] Harry is round.[(triple4)] @1: Bob is cold.[(((triple1) -> rule1))] Fiona is cold.[(((triple3) -> rule1))] @2: Bob is round.[(((((triple1) -> rule1)) -> rule7))] Fiona is round.[(((((triple3) -> rule1)) -> rule7))] @3: Fiona is green.[(((((((triple3) -> rule1)) -> rule7)) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3