Bob is green. Erin is not quiet. Fiona is quiet. Harry is not green. Quiet people are not red. All quiet people are green. Green people are young. Big people are quiet. Green people are big. Blue, young people are big. If someone is young and not red then they are white. Young, big people are white.
Bob is green.
("Bob" "is" "green" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is not green.
("Harry" "is" "green" "-")
Quiet people are not red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Blue, young people are big.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young and not red then they are white.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "+"))
Young, big people are white.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Harry is not green.
True
1
proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Harry is green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "+")
triple4
Fiona is green.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "green" "+")
((triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "young" "-")
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is young.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Bob is not white.
False
5
inv-proof
[(((((triple1) -> rule3) ((triple1) -> rule5)) -> rule8) OR ((((triple1) -> rule3) ((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7))]
("Bob" "is" "white" "-")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple1) -> (rule3 % int5)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Bob is not red.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "red" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "white" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is green.[(triple1)] Erin is not quiet.[(triple2)] Fiona is quiet.[(triple3)] Harry is not green.[(triple4)] @1: Bob is big.[(((triple1) -> rule5))] Bob is young.[(((triple1) -> rule3))] Fiona is green.[(((triple3) -> rule2))] Fiona is not red.[(((triple3) -> rule1))] @2: Bob is quiet.[(((((triple1) -> rule5)) -> rule4))] Bob is white.[(((((triple1) -> rule3) ((triple1) -> rule5)) -> rule8) OR ((((triple1) -> rule3) ((((((triple1) -> rule5)) -> rule4)) -> rule1)) -> rule7))] Fiona is big.[(((((triple3) -> rule2)) -> rule5))] Fiona is young.[(((((triple3) -> rule2)) -> rule3))] @3: Bob is not red.[(((((((triple1) -> rule5)) -> rule4)) -> rule1))] Fiona is white.[(((((((triple3) -> rule2)) -> rule3) ((triple3) -> rule1)) -> rule7) OR ((((((triple3) -> rule2)) -> rule3) ((((triple3) -> rule2)) -> rule5)) -> rule8))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Harry is not green.
("Harry" "is" "green" "-")
triple4
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
((triple3) -> (rule1 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple1) -> (rule3 % int5)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Fiona is big.
("Fiona" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Bob is not red.
("Bob" "is" "red" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple3) -> (rule2 % int4))) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((((triple3) -> (rule2 % int4))) -> (rule3 % int3)) ((((triple3) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4