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