Charlie is smart. Charlie is white. Charlie is young. Erin is cold. Erin is smart. Harry is cold. Harry is red. Smart people are blue. If someone is cold and red then they are white. If Erin is smart and Erin is blue then Erin is kind.
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and red then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If Erin is smart and Erin is blue then Erin is kind.
((("Erin" "is" "smart" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
Erin is smart.
True
1
proof
[(triple5)]
("Erin" "is" "smart" "+")
triple5
Harry is not cold.
False
1
inv-proof
[(triple6)]
("Harry" "is" "cold" "-")
triple6
Charlie is blue.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is not white.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("Harry" "is" "white" "-")
((triple6 triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is kind.
True
4
proof
[(((triple5 ((triple5) -> rule1)) -> rule3))]
("Erin" "is" "kind" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((triple5 ((triple5) -> rule1)) -> rule3))]
("Erin" "is" "kind" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Charlie is smart.[(triple1)] Charlie is white.[(triple2)] Charlie is young.[(triple3)] Erin is cold.[(triple4)] Erin is smart.[(triple5)] Harry is cold.[(triple6)] Harry is red.[(triple7)] @1: Charlie is blue.[(((triple1) -> rule1))] Erin is blue.[(((triple5) -> rule1))] Harry is white.[(((triple6 triple7) -> rule2))] @2: Erin is kind.[(((triple5 ((triple5) -> rule1)) -> rule3))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6 triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2