Charlie is big. Charlie is blue. Charlie is nice. Charlie is red. Charlie is rough. Charlie is smart. Charlie is young. Dave is big. Dave is red. Dave is young. Erin is big. Erin is blue. Erin is nice. Erin is red. Erin is rough. Erin is young. All nice, blue things are big. Nice things are rough. If Erin is rough then Erin is smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
All nice, blue things are big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Erin is rough then Erin is smart.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
Dave is big.
True
1
proof
[(triple8)]
("Dave" "is" "big" "+")
triple8
Erin is not blue.
False
1
inv-proof
[(triple12)]
("Erin" "is" "blue" "-")
triple12
Erin is smart.
True
2
proof
[(((triple15) -> rule3) OR ((((triple13) -> rule2)) -> rule3))]
("Erin" "is" "smart" "+")
((triple15) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple15) -> rule3) OR ((((triple13) -> rule2)) -> rule3))]
("Erin" "is" "smart" "-")
((triple15) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is big.[(triple1 OR ((triple3 triple2) -> rule1))] Charlie is blue.[(triple2)] Charlie is nice.[(triple3)] Charlie is red.[(triple4)] Charlie is rough.[(triple5 OR ((triple3) -> rule2))] Charlie is smart.[(triple6)] Charlie is young.[(triple7)] Dave is big.[(triple8)] Dave is red.[(triple9)] Dave is young.[(triple10)] Erin is big.[(triple11 OR ((triple13 triple12) -> rule1))] Erin is blue.[(triple12)] Erin is nice.[(triple13)] Erin is red.[(triple14)] Erin is rough.[(triple15 OR ((triple13) -> rule2))] Erin is young.[(triple16)] @1: Erin is smart.[(((triple15) -> rule3) OR ((((triple13) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 triple2) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple13 triple12) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
triple13
Erin is red.
("Erin" "is" "red" "+")
triple14
Erin is rough.
("Erin" "is" "rough" "+")
triple15
((triple13) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple16
Erin is smart.
("Erin" "is" "smart" "+")
((triple15) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2