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