Bob is nice. Fiona is cold. Gary is green. If someone is nice then they are big. All big, green people are white. If Fiona is white and Fiona is quiet then Fiona is nice. All red people are nice. All cold people are red. All big, nice people are cold.
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All big, green people are white.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Fiona is white and Fiona is quiet then Fiona is nice.
((("Fiona" "is" "white" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "nice" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All big, nice people are cold.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Fiona is red.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "red" "+")
((triple2) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "red" "-")
((triple2) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Fiona" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("Fiona" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Bob is red.
True
5
proof
[(((((((triple1) -> rule1) triple1) -> rule6)) -> rule5))]
("Bob" "is" "red" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not red.
False
5
inv-proof
[(((((((triple1) -> rule1) triple1) -> rule6)) -> rule5))]
("Bob" "is" "red" "-")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@5: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "+")
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is nice.[(triple1)] Fiona is cold.[(triple2)] Gary is green.[(triple3)] @1: Bob is big.[(((triple1) -> rule1))] Fiona is red.[(((triple2) -> rule5))] @2: Bob is cold.[(((((triple1) -> rule1) triple1) -> rule6))] Fiona is nice.[(((((triple2) -> rule5)) -> rule4))] @3: Bob is red.[(((((((triple1) -> rule1) triple1) -> rule6)) -> rule5))] Fiona is big.[(((((((triple2) -> rule5)) -> rule4)) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple2) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3