Erin is blue. Erin is kind. Erin is nice. Erin is not round. Erin is smart. Harry is nice. Harry is smart. If Harry is smart then Harry is round. If Harry is round then Harry is young.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is smart then Harry is round.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "+"))
If Harry is round then Harry is young.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "young" "+"))
Erin is smart.
True
1
proof
[(triple5)]
("Erin" "is" "smart" "+")
triple5
Erin is not nice.
False
1
inv-proof
[(triple3)]
("Erin" "is" "nice" "-")
triple3
Harry is round.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "round" "-")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("Harry" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Harry" "is" "young" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Erin is blue.[(triple1)] Erin is kind.[(triple2)] Erin is nice.[(triple3)] Erin is not round.[(triple4)] Erin is smart.[(triple5)] Harry is nice.[(triple6)] Harry is smart.[(triple7)] @1: Harry is round.[(((triple7) -> rule1))] @2: Harry is young.[(((((triple7) -> rule1)) -> rule2))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is not round.
("Erin" "is" "round" "-")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2