Bob is not big. Bob is green. Bob is smart. Dave is green. Fiona is big. Fiona is not smart. Gary is big. If something is blue then it is rough. If something is smart then it is red. Green things are blue. Rough things are smart. If something is green and not blue then it is big. Red things are not big. If something is rough and big then it is kind. If something is smart and not blue then it is kind. If something is blue then it is kind.
Bob is not big.
("Bob" "is" "big" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Gary is big.
("Gary" "is" "big" "+")
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is green and not blue then it is big.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "+"))
Red things are not big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "-"))
If something is rough and big then it is kind.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is smart and not blue then it is kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Bob is smart.
True
1
proof
[(triple3 OR ((((((triple2) -> rule3)) -> rule1)) -> rule4))]
("Bob" "is" "smart" "+")
triple3
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is big.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule2)) -> rule6) OR ((((((((((triple2) -> rule3)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
("Bob" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((((((triple2) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5
Bob is blue.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule9))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple4) -> rule3)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule1)) -> rule4))]
("Dave" "is" "smart" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
True
5
proof
[(((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "red" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not red.
False
5
inv-proof
[(((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "red" "-")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not big.
True
6
proof
[(((((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "big" "-")
((((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is big.
False
6
inv-proof
[(((((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "big" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Gary is smart.
Unknown
rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is kind.
Unknown
rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is green.[(triple2)] Bob is not big.[(triple1 OR ((((triple3) -> rule2)) -> rule6) OR ((((((((((triple2) -> rule3)) -> rule1)) -> rule4)) -> rule2)) -> rule6))] Bob is smart.[(triple3 OR ((((((triple2) -> rule3)) -> rule1)) -> rule4))] Dave is green.[(triple4)] Fiona is big.[(triple5)] Fiona is not smart.[(triple6)] Gary is big.[(triple7)] @1: Bob is blue.[(((triple2) -> rule3))] Bob is red.[(((triple3) -> rule2) OR ((((((((triple2) -> rule3)) -> rule1)) -> rule4)) -> rule2))] Dave is blue.[(((triple4) -> rule3))] @2: Bob is kind.[(((((triple2) -> rule3)) -> rule9))] Bob is rough.[(((((triple2) -> rule3)) -> rule1))] Dave is kind.[(((((triple4) -> rule3)) -> rule9))] Dave is rough.[(((((triple4) -> rule3)) -> rule1))] @3: Dave is smart.[(((((((triple4) -> rule3)) -> rule1)) -> rule4))] @4: Dave is red.[(((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2))] @5: Dave is not big.[(((((((((((triple4) -> rule3)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not big.
("Bob" "is" "big" "-")
triple1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((((((triple2) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule9 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4) -> (rule3 % int2))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not big.
("Dave" "is" "big" "-")
((((((((((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5