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