Bob is blue. Dave is kind. Dave is white. Fiona is big. Fiona is not blue. Gary is blue. Gary is kind. Gary is smart. Gary is white. Gary is young. If Dave is big then Dave is not blue. All white people are big. If someone is white and not blue then they are nice. All nice, kind people are smart. If someone is blue and not nice then they are smart. If someone is smart and not blue then they are young.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is big then Dave is not blue.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "-"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is white and not blue then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "+"))
All nice, kind people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and not nice then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "smart" "+"))
If someone is smart and not blue then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
Gary is kind.
True
1
proof
[(triple7)]
("Gary" "is" "kind" "+")
triple7
Gary is not smart.
False
1
inv-proof
[(triple8)]
("Gary" "is" "smart" "-")
triple8
Gary is big.
True
2
proof
[(((triple9) -> rule2))]
("Gary" "is" "big" "+")
((triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "big" "-")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
True
7
proof
[(((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4))]
("Dave" "is" "smart" "+")
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not smart.
False
7
inv-proof
[(((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4))]
("Dave" "is" "smart" "-")
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is young.
True
11
proof
[(((((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4) ((((triple3) -> rule2)) -> rule1)) -> rule6))]
("Dave" "is" "young" "+")
((((((triple3 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple2) -> (rule4 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Dave is not young.
False
11
inv-proof
[(((((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4) ((((triple3) -> rule2)) -> rule1)) -> rule6))]
("Dave" "is" "young" "-")
((((((triple3 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple2) -> (rule4 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is blue.[(triple1)] Dave is kind.[(triple2)] Dave is white.[(triple3)] Fiona is big.[(triple4)] Fiona is not blue.[(triple5)] Gary is blue.[(triple6)] Gary is kind.[(triple7)] Gary is smart.[(triple8)] Gary is white.[(triple9)] Gary is young.[(triple10)] @1: Dave is big.[(((triple3) -> rule2))] Gary is big.[(((triple9) -> rule2))] @2: Dave is not blue.[(((((triple3) -> rule2)) -> rule1))] @3: Dave is nice.[(((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3))] @4: Dave is smart.[(((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4))] @5: Dave is young.[(((((((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule3) triple2) -> rule4) ((((triple3) -> rule2)) -> rule1)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Gary is white.
("Gary" "is" "white" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((((triple3 ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple2) -> (rule4 % int2)) ((((triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
int4
Dave is big.
("Dave" "is" "big" "+")
int5