Charlie is not big. Charlie is nice. Charlie is not smart. Erin is blue. Erin is red. Erin is not smart. Harry is green. Green, smart things are red. If something is blue and big then it is not nice. If something is green then it is smart. If something is smart and not blue then it is not big. Red things are big. If something is big and not blue then it is green.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Harry is green.
("Harry" "is" "green" "+")
Green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is blue and big then it is not nice.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not blue then it is not big.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "-"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is big and not blue then it is green.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple5)]
("Erin" "is" "red" "+")
triple5
Erin is not red.
False
1
inv-proof
[(triple5)]
("Erin" "is" "red" "-")
triple5
Harry is smart.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "smart" "-")
((triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is not nice.
True
4
proof
[(((triple4 ((triple5) -> rule5)) -> rule2))]
("Erin" "is" "nice" "-")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
False
4
inv-proof
[(((triple4 ((triple5) -> rule5)) -> rule2))]
("Erin" "is" "nice" "+")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is big.
True
5
proof
[(((((triple7 ((triple7) -> rule3)) -> rule1)) -> rule5))]
("Harry" "is" "big" "+")
((((triple7 ((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule3)) -> rule1)) -> rule5))]
("Harry" "is" "big" "-")
((((triple7 ((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Charlie is nice.[(triple2)] Charlie is not big.[(triple1)] Charlie is not smart.[(triple3)] Erin is blue.[(triple4)] Erin is not smart.[(triple6)] Erin is red.[(triple5)] Harry is green.[(triple7)] @1: Erin is big.[(((triple5) -> rule5))] Harry is smart.[(((triple7) -> rule3))] @2: Erin is not nice.[(((triple4 ((triple5) -> rule5)) -> rule2))] Harry is red.[(((triple7 ((triple7) -> rule3)) -> rule1))] @3: Harry is big.[(((((triple7 ((triple7) -> rule3)) -> rule1)) -> rule5))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
((triple5) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple7 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple7 ((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3