Dave is green. Dave is quiet. Dave is young. Erin is big. Erin is kind. Erin is white. Fiona is big. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is smart. Fiona is white. Fiona is young. Gary is smart. Gary is white. Gary is young. Big things are young. Green things are big. All big, green things are smart.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All big, green things are smart.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Fiona is smart.
True
1
proof
[(triple11 OR ((triple7 triple8) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3))]
("Fiona" "is" "smart" "+")
triple11
((triple7 triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is not big.
False
1
inv-proof
[(triple4)]
("Erin" "is" "big" "-")
triple4
Erin is young.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "-")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Dave is smart.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is green.[(triple1)] Dave is quiet.[(triple2)] Dave is young.[(triple3 OR ((((triple1) -> rule2)) -> rule1))] Erin is big.[(triple4)] Erin is kind.[(triple5)] Erin is white.[(triple6)] Fiona is big.[(triple7 OR ((triple8) -> rule2))] Fiona is green.[(triple8)] Fiona is kind.[(triple9)] Fiona is quiet.[(triple10)] Fiona is smart.[(triple11 OR ((triple7 triple8) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3))] Fiona is white.[(triple12)] Fiona is young.[(triple13 OR ((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Gary is smart.[(triple14)] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Dave is big.[(((triple1) -> rule2))] Erin is young.[(((triple4) -> rule1))] @2: Dave is smart.[(((((triple1) -> rule2) triple1) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple8) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple7 triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Fiona is young.
("Fiona" "is" "young" "+")
triple13
((triple7) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2