Dave is green. Erin is blue. Fiona is green. Fiona is kind. Fiona is smart. Harry is rough. Harry is smart. Smart things are rough. All blue, quiet things are rough. Big things are kind. If Erin is blue then Erin is big. Kind things are green. All green, big things are smart.
Dave is green.
("Dave" "is" "green" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All blue, quiet things are rough.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Erin is blue then Erin is big.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "big" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All green, big things are smart.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "smart" "-")
triple5
Erin is big.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "big" "+")
((triple2) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Fiona" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
True
4
proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "green" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not green.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule5))]
("Erin" "is" "green" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
True
7
proof
[(((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6))]
("Erin" "is" "smart" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int4))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is not smart.
False
7
inv-proof
[(((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6))]
("Erin" "is" "smart" "-")
((((((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int4))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is rough.
True
8
proof
[(((((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6)) -> rule1))]
("Erin" "is" "rough" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Erin is not rough.
False
8
inv-proof
[(((((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6)) -> rule1))]
("Erin" "is" "rough" "-")
((((((((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is green.[(triple1)] Erin is blue.[(triple2)] Fiona is green.[(triple3 OR ((triple4) -> rule5))] Fiona is kind.[(triple4)] Fiona is smart.[(triple5)] Harry is rough.[(triple6 OR ((triple7) -> rule1))] Harry is smart.[(triple7)] @1: Erin is big.[(((triple2) -> rule4))] Fiona is rough.[(((triple5) -> rule1))] @2: Erin is kind.[(((((triple2) -> rule4)) -> rule3))] @3: Erin is green.[(((((((triple2) -> rule4)) -> rule3)) -> rule5))] @4: Erin is smart.[(((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6))] @5: Erin is rough.[(((((((((((triple2) -> rule4)) -> rule3)) -> rule5) ((triple2) -> rule4)) -> rule6)) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((triple4) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((triple7) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int4))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int5))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5