Dave is green. Dave is kind. Dave is quiet. Erin is green. Erin is quiet. Erin is rough. Erin is smart. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is smart. Harry is smart. If Erin is young and Erin is quiet then Erin is red. All rough people are quiet. Smart, red people are young. If someone is green and young then they are rough. Smart people are rough. If Dave is red then Dave is kind.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Erin is young and Erin is quiet then Erin is red.
((("Erin" "is" "young" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "red" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Smart, red people are young.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is green and young then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Dave is red then Dave is kind.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "kind" "+"))
Erin is quiet.
True
1
proof
[(triple5 OR ((triple6) -> rule2) OR ((((triple7) -> rule5)) -> rule2))]
("Erin" "is" "quiet" "+")
triple5
((triple6) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule5))]
("Erin" "is" "rough" "-")
triple6
((triple7) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is green.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] Erin is green.[(triple4)] Erin is quiet.[(triple5 OR ((triple6) -> rule2) OR ((((triple7) -> rule5)) -> rule2))] Erin is rough.[(triple6 OR ((triple7) -> rule5))] Erin is smart.[(triple7)] Fiona is quiet.[(triple8 OR ((triple10) -> rule2) OR ((((triple11) -> rule5)) -> rule2))] Fiona is red.[(triple9)] Fiona is rough.[(triple10 OR ((triple11) -> rule5))] Fiona is smart.[(triple11)] Harry is smart.[(triple12)] @1: Fiona is young.[(((triple11 triple9) -> rule3))] Harry is rough.[(((triple12) -> rule5))] @2: Harry is quiet.[(((((triple12) -> rule5)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple6) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple7) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
((triple10) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
((triple11) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Fiona is young.
("Fiona" "is" "young" "+")
((triple11 triple9) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2