Bob is kind. Bob is red. Bob is rough. Erin is red. Fiona is rough. Fiona is white. Harry is round. White, rough people are big. If Harry is big and Harry is round then Harry is white. Red people are rough. If someone is round then they are rough. All rough people are white. If Erin is big and Erin is not rough then Erin is not quiet. If someone is quiet and round then they are kind. If someone is red and not big then they are not quiet. Big, round people are quiet.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
White, rough people are big.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Harry is big and Harry is round then Harry is white.
((("Harry" "is" "big" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Erin is big and Erin is not rough then Erin is not quiet.
((("Erin" "is" "big" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "quiet" "-"))
If someone is quiet and round then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not big then they are not quiet.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "-"))
Big, round people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Fiona is white.
True
1
proof
[(triple6 OR ((triple5) -> rule5))]
("Fiona" "is" "white" "+")
triple6
((triple5) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not rough.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "rough" "-")
triple5
Erin is rough.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is big.
True
4
proof
[(((((triple3) -> rule5) triple3) -> rule1) OR ((((triple3) -> rule5) ((triple2) -> rule3)) -> rule1) OR ((((((triple2) -> rule3)) -> rule5) triple3) -> rule1) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "big" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Erin is not white.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Erin" "is" "white" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Harry is big.
True
6
proof
[(((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1))]
("Harry" "is" "big" "+")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) ((triple7) -> (rule4 % int3))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not big.
False
6
inv-proof
[(((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1))]
("Harry" "is" "big" "-")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) ((triple7) -> (rule4 % int3))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
True
8
proof
[(((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9))]
("Harry" "is" "quiet" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) ((triple7) -> (rule4 % int4))) -> (rule1 % int2)) triple7) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not quiet.
False
8
inv-proof
[(((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9))]
("Harry" "is" "quiet" "-")
((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) ((triple7) -> (rule4 % int4))) -> (rule1 % int2)) triple7) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is kind.
True
10
proof
[(((((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9) triple7) -> rule7))]
("Harry" "is" "kind" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) ((triple7) -> (rule4 % int5))) -> (rule1 % int3)) triple7) -> (rule9 % int2)) triple7) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is not kind.
False
10
inv-proof
[(((((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9) triple7) -> rule7))]
("Harry" "is" "kind" "-")
((((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) ((triple7) -> (rule4 % int5))) -> (rule1 % int3)) triple7) -> (rule9 % int2)) triple7) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is kind.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3 OR ((triple2) -> rule3))] Erin is red.[(triple4)] Fiona is rough.[(triple5)] Fiona is white.[(triple6 OR ((triple5) -> rule5))] Harry is round.[(triple7)] @1: Bob is white.[(((triple3) -> rule5) OR ((((triple2) -> rule3)) -> rule5))] Erin is rough.[(((triple4) -> rule3))] Fiona is big.[(((triple6 triple5) -> rule1) OR ((((triple5) -> rule5) triple5) -> rule1))] Harry is rough.[(((triple7) -> rule4))] @2: Bob is big.[(((((triple3) -> rule5) triple3) -> rule1) OR ((((triple3) -> rule5) ((triple2) -> rule3)) -> rule1) OR ((((((triple2) -> rule3)) -> rule5) triple3) -> rule1) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule1))] Erin is white.[(((((triple4) -> rule3)) -> rule5))] Harry is white.[(((((triple7) -> rule4)) -> rule5))] @3: Erin is big.[(((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule3)) -> rule1))] Harry is big.[(((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1))] @4: Harry is quiet.[(((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9))] @5: Harry is kind.[(((((((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule1) triple7) -> rule9) triple7) -> rule7))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
((triple5) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple6 triple5) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple5) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) ((triple7) -> (rule4 % int3))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule5 % int3)) ((triple7) -> (rule4 % int4))) -> (rule1 % int2)) triple7) -> (rule9 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule5 % int4)) ((triple7) -> (rule4 % int5))) -> (rule1 % int3)) triple7) -> (rule9 % int2)) triple7) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5