Charlie is blue. Dave is young. Erin is round. Fiona is big. If someone is blue then they are young. If Charlie is big and Charlie is young then Charlie is rough. If someone is big and green then they are white. If someone is young then they are round. If someone is young then they are big. All blue, young people are white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If Charlie is big and Charlie is young then Charlie is rough.
((("Charlie" "is" "big" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is big and green then they are white.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All blue, young people are white.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Fiona is big.
True
1
proof
[(triple4)]
("Fiona" "is" "big" "+")
triple4
Fiona is not big.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "big" "-")
triple4
Dave is big.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "big" "+")
((triple2) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "round" "-")
((triple2) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Charlie is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "white" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
True
6
proof
[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not rough.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Dave is young.[(triple2)] Erin is round.[(triple3)] Fiona is big.[(triple4)] @1: Charlie is young.[(((triple1) -> rule1))] Dave is big.[(((triple2) -> rule5))] Dave is round.[(((triple2) -> rule4))] @2: Charlie is big.[(((((triple1) -> rule1)) -> rule5))] Charlie is round.[(((((triple1) -> rule1)) -> rule4))] Charlie is white.[(((triple1 ((triple1) -> rule1)) -> rule6))] @3: Charlie is rough.[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3