Charlie is not big. Charlie is cold. Erin is big. Erin is white. Fiona is big. Fiona is kind. Harry is big. If something is big and white then it is young. If Erin is not young then Erin is smart. If something is red then it is kind. Big, white things are smart. Red things are not smart. If something is smart and not white then it is red.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is big and white then it is young.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Erin is not young then Erin is smart.
((("Erin" "is" "young" "~")) -> ("Erin" "is" "smart" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Big, white things are smart.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Red things are not smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
If something is smart and not white then it is red.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "red" "+"))
Harry is big.
True
1
proof
[(triple7)]
("Harry" "is" "big" "+")
triple7
Harry is not big.
False
1
inv-proof
[(triple7)]
("Harry" "is" "big" "-")
triple7
Erin is smart.
True
3
proof
[(((triple3 triple4) -> rule4))]
("Erin" "is" "smart" "+")
((triple3 triple4) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not young.
False
3
inv-proof
[(((triple3 triple4) -> rule1))]
("Erin" "is" "young" "-")
((triple3 triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is cold.[(triple2)] Charlie is not big.[(triple1)] Erin is big.[(triple3)] Erin is white.[(triple4)] Fiona is big.[(triple5)] Fiona is kind.[(triple6)] Harry is big.[(triple7)] @1: Erin is smart.[(((triple3 triple4) -> rule4))] Erin is young.[(((triple3 triple4) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple3 triple4) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple3 triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1