Dave is quiet. Dave is smart. Erin is big. Erin is quiet. Erin is young. Harry is big. Harry is green. Harry is quiet. Harry is smart. Harry is white. If someone is big then they are green. All young, quiet people are smart.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All young, quiet people are smart.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Erin is big.
True
1
proof
[(triple3)]
("Erin" "is" "big" "+")
triple3
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2)] Erin is big.[(triple3)] Erin is quiet.[(triple4)] Erin is young.[(triple5)] Harry is big.[(triple6)] Harry is green.[(triple7 OR ((triple6) -> rule1))] Harry is quiet.[(triple8)] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Erin is green.[(((triple3) -> rule1))] Erin is smart.[(((triple5 triple4) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 triple4) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1