Charlie is nice. Erin is cold. Erin is kind. Erin is rough. Erin is smart. Fiona is kind. Fiona is nice. Fiona is red. Fiona is rough. Harry is cold. Harry is nice. Harry is smart. All smart, nice things are rough. All smart, red things are green. If something is smart then it is red.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart, nice things are rough.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All smart, red things are green.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Fiona is not nice.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "nice" "-")
triple7
Harry is red.
True
2
proof
[(((triple12) -> rule3))]
("Harry" "is" "red" "+")
((triple12) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "red" "-")
((triple5) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is nice.[(triple1)] Erin is cold.[(triple2)] Erin is kind.[(triple3)] Erin is rough.[(triple4)] Erin is smart.[(triple5)] Fiona is kind.[(triple6)] Fiona is nice.[(triple7)] Fiona is red.[(triple8)] Fiona is rough.[(triple9)] Harry is cold.[(triple10)] Harry is nice.[(triple11)] Harry is smart.[(triple12)] @1: Erin is red.[(((triple5) -> rule3))] Harry is red.[(((triple12) -> rule3))] Harry is rough.[(((triple12 triple11) -> rule1))] @2: Erin is green.[(((triple5 ((triple5) -> rule3)) -> rule2))] Harry is green.[(((triple12 ((triple12) -> rule3)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Erin is red.
("Erin" "is" "red" "+")
((triple5) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12 triple11) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple12 ((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2