Charlie is blue. Charlie is cold. Charlie is kind. Charlie is red. Erin is big. Fiona is big. Fiona is blue. Red things are blue. Red things are cold. If something is kind and red then it is nice. If Fiona is red and Fiona is big then Fiona is blue. Nice things are red. If Charlie is blue and Charlie is big then Charlie is red. All cold things are kind. All nice things are cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is kind and red then it is nice.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Fiona is red and Fiona is big then Fiona is blue.
((("Fiona" "is" "red" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "blue" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Charlie is blue and Charlie is big then Charlie is red.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple2) -> rule7) OR ((((triple4) -> rule2)) -> rule7))]
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Fiona is not blue.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "blue" "-")
triple7
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is blue.[(triple1 OR ((triple4) -> rule1))] Charlie is cold.[(triple2 OR ((triple4) -> rule2) OR ((((triple3 triple4) -> rule3)) -> rule8))] Charlie is kind.[(triple3 OR ((triple2) -> rule7) OR ((((triple4) -> rule2)) -> rule7))] Charlie is red.[(triple4)] Erin is big.[(triple5)] Fiona is big.[(triple6)] Fiona is blue.[(triple7)] @1: Charlie is nice.[(((triple3 triple4) -> rule3) OR ((((triple2) -> rule7) triple4) -> rule3) OR ((((((triple4) -> rule2)) -> rule7) triple4) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple4) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3 triple4) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3 triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3