Bob is blue. Bob is cold. Bob is nice. Charlie is green. Erin is big. Erin is green. Erin is quiet. Erin is young. Fiona is blue. Fiona is green. Fiona is nice. Fiona is young. If something is young then it is blue. If something is young and blue then it is cold. Cold things are nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is young and blue then it is cold.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Erin is big.
True
1
proof
[(triple5)]
("Erin" "is" "big" "+")
triple5
Erin is not green.
False
1
inv-proof
[(triple6)]
("Erin" "is" "green" "-")
triple6
Fiona is cold.
True
3
proof
[(((triple12 triple9) -> rule2) OR ((triple12 ((triple12) -> rule1)) -> rule2))]
("Fiona" "is" "cold" "+")
((triple12 triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple12 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((triple12 triple9) -> rule2) OR ((triple12 ((triple12) -> rule1)) -> rule2))]
("Fiona" "is" "cold" "-")
((triple12 triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple12 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Erin is cold.
True
4
proof
[(((triple8 ((triple8) -> rule1)) -> rule2))]
("Erin" "is" "cold" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((triple8 ((triple8) -> rule1)) -> rule2))]
("Erin" "is" "cold" "-")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
True
5
proof
[(((((triple8 ((triple8) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((((triple8 ((triple8) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "nice" "-")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is nice.[(triple3 OR ((triple2) -> rule3))] Charlie is green.[(triple4)] Erin is big.[(triple5)] Erin is green.[(triple6)] Erin is quiet.[(triple7)] Erin is young.[(triple8)] Fiona is blue.[(triple9 OR ((triple12) -> rule1))] Fiona is green.[(triple10)] Fiona is nice.[(triple11 OR ((((triple12 triple9) -> rule2)) -> rule3) OR ((((triple12 ((triple12) -> rule1)) -> rule2)) -> rule3))] Fiona is young.[(triple12)] @1: Erin is blue.[(((triple8) -> rule1))] Fiona is cold.[(((triple12 triple9) -> rule2) OR ((triple12 ((triple12) -> rule1)) -> rule2))] @2: Erin is cold.[(((triple8 ((triple8) -> rule1)) -> rule2))] @3: Erin is nice.[(((((triple8 ((triple8) -> rule1)) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple12) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((((triple12 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple12 ((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
((triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple12 triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple12 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3