Erin is kind. Erin is rough. Harry is blue. Harry is nice. Harry is not rough. Harry is smart. Harry is young. If someone is blue and nice then they are smart. All blue, green people are smart. If someone is rough and not young then they are smart. All rough, green people are blue. If Erin is nice then Erin is blue. If someone is rough then they are green.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is blue and nice then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All blue, green people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough and not young then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "smart" "+"))
All rough, green people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Erin is nice then Erin is blue.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "blue" "+"))
If someone is rough then they are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Erin is kind.
True
1
proof
[(triple1)]
("Erin" "is" "kind" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Erin is green.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "-")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule4))]
("Erin" "is" "blue" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule4))]
("Erin" "is" "blue" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
True
7
proof
[(((((triple2 ((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule2))]
("Erin" "is" "smart" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not smart.
False
7
inv-proof
[(((((triple2 ((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule2))]
("Erin" "is" "smart" "-")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Erin is kind.[(triple1)] Erin is rough.[(triple2)] Harry is blue.[(triple3)] Harry is nice.[(triple4)] Harry is not rough.[(triple5)] Harry is smart.[(triple6 OR ((triple3 triple4) -> rule1))] Harry is young.[(triple7)] @1: Erin is green.[(((triple2) -> rule6))] @2: Erin is blue.[(((triple2 ((triple2) -> rule6)) -> rule4))] @3: Erin is smart.[(((((triple2 ((triple2) -> rule6)) -> rule4) ((triple2) -> rule6)) -> rule2))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is not rough.
("Harry" "is" "rough" "-")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((triple3 triple4) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3