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