Bob is red. Fiona is red. Gary is big. All red things are young. If Fiona is red then Fiona is big. If Gary is big then Gary is quiet. If Gary is not young then Gary is quiet. All kind things are cold. All white things are cold. If something is kind and not big then it is cold. All quiet things are kind.
Bob is red.
("Bob" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Fiona is red then Fiona is big.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "big" "+"))
If Gary is big then Gary is quiet.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "quiet" "+"))
If Gary is not young then Gary is quiet.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "quiet" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is kind and not big then it is cold.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
All quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Gary is not big.
False
1
inv-proof
[(triple3)]
("Gary" "is" "big" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
True
3
proof
[(((((triple3) -> rule3)) -> rule8))]
("Gary" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule8))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
True
4
proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
("Gary" "is" "cold" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is cold.
Unknown
rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Fiona" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Bob is red.[(triple1)] Fiona is red.[(triple2)] Gary is big.[(triple3)] @1: Bob is young.[(((triple1) -> rule1))] Fiona is big.[(((triple2) -> rule2))] Fiona is young.[(((triple2) -> rule1))] Gary is quiet.[(((triple3) -> rule3))] @2: Gary is kind.[(((((triple3) -> rule3)) -> rule8))] @3: Gary is cold.[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple2) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3